← Mathematical handbook

Tables 1–3: Nelsen 13 constructor, endpoints, orders, CI, and tails

theorem Papers.AnsariRockel2024.nelsen13_cdf (θ : ℝ) (hθ : 0 < θ) (u v : ↑unitInterval) : (Verification.nelsen13 θ ⋯).cdf ![u, v] = if u = 0 ∨ v = 0 then 0 else Real.exp (1 - ((1 - Real.log ↑u) ^ θ + (1 - Real.log ↑v) ^ θ - 1) ^ θ⁻¹)

theorem Papers.AnsariRockel2024.nelsen13_zero : Verification.nelsen13 0 ⋯ = Verification.gumbelBarnett 1

theorem Papers.AnsariRockel2024.nelsen13_one : Verification.nelsen13 1 ⋯ = ProbabilityTheory.Copula.independence 2

theorem Papers.AnsariRockel2024.nelsen13_tails (θ : ℝ) (hθ : 0 ≤ θ) : (Verification.nelsen13 θ hθ).HasLowerTailDependence 0 ∧ (Verification.nelsen13 θ hθ).HasUpperTailDependence 0

theorem Papers.AnsariRockel2024.nelsen13_lowerOrthant_monotone {θ η : ℝ} (hθ : 0 ≤ θ) (hη : 0 ≤ η) (hθη : θ ≤ η) : (Verification.nelsen13 θ hθ).LowerOrthantLE (Verification.nelsen13 η hη)

theorem Papers.AnsariRockel2024.nelsen13_tendsto_zero {α : Type u_1} {l : Filter α} (θ : α → ℝ) (hθ : ∀ (z : α), 0 ≤ θ z) (hlim : Filter.Tendsto θ l (nhds 0)) (u v : ↑unitInterval) : Filter.Tendsto (fun (z : α) => (Verification.nelsen13 (θ z) ⋯).cdf ![u, v]) l (nhds ((Verification.gumbelBarnett 1).cdf ![u, v]))

theorem Papers.AnsariRockel2024.nelsen13_tendsto_atTop {α : Type u_1} {l : Filter α} (θ : α → ℝ) (hθ : ∀ (z : α), 0 ≤ θ z) (hlim : Filter.Tendsto θ l Filter.atTop) (u v : ↑unitInterval) : Filter.Tendsto (fun (z : α) => (Verification.nelsen13 (θ z) ⋯).cdf ![u, v]) l (nhds (min ↑u ↑v))

theorem Papers.AnsariRockel2024.nelsen13_ci_iff (θ : ℝ) (hθ : 0 ≤ θ) : (Verification.nelsen13 θ hθ).IsCI ↔ 1 ≤ θ

theorem Papers.AnsariRockel2024.nelsen13_schur_monotone {θ η : ℝ} (hθ : 1 ≤ θ) (hη : 1 ≤ η) (hθη : θ ≤ η) : (Verification.nelsen13 θ ⋯).SchurBothLE (Verification.nelsen13 η ⋯)

theorem Papers.AnsariRockel2024.nelsen13_density_tp2_requires_one (θ : ℝ) (hθ : 0 ≤ θ) (hd : (Verification.nelsen13 θ hθ).HasMTP2Density) : 1 ≤ θ

theorem Papers.AnsariRockel2024.nelsen13_density_measure {θ : ℝ} (hθ : 1 ≤ θ) : (Verification.nelsen13 θ ⋯).toMeasure = MeasureTheory.volume.withDensity fun (x : Fin 2 → ↑unitInterval) => ENNReal.ofReal (Verification.n13Density θ x)

theorem Papers.AnsariRockel2024.nelsen13_density_tp2_iff (θ : ℝ) (hθ : 0 ≤ θ) : (Verification.nelsen13 θ hθ).HasMTP2Density ↔ 1 ≤ θ