← Mathematical handbook

Tables 1–3: Nelsen 19 constructor, zero limit, CI and tails

theorem Papers.AnsariRockel2024.nelsen19_cdf {θ : ℝ} (hθ : 0 < θ) (u v : ↑unitInterval) : (Verification.nelsen19 θ ⋯).cdf ![u, v] = if u = 0 ∨ v = 0 then 0 else θ / Real.log (Real.exp (θ / ↑u) + Real.exp (θ / ↑v) - Real.exp θ)

theorem Papers.AnsariRockel2024.nelsen19_zero : Verification.nelsen19 0 ⋯ = ProbabilityTheory.Copula.clayton 2 1 ⋯

theorem Papers.AnsariRockel2024.nelsen19_ci (θ : ℝ) (hθ : 0 ≤ θ) : (Verification.nelsen19 θ hθ).IsCI

theorem Papers.AnsariRockel2024.nelsen19_tails (θ : ℝ) (hθ : 0 ≤ θ) : (Verification.nelsen19 θ hθ).HasLowerTailDependence (if θ = 0 then 1 / 2 else 1) ∧ (Verification.nelsen19 θ hθ).HasUpperTailDependence 0

theorem Papers.AnsariRockel2024.nelsen19_tendsto_zero {α : Type u_1} {l : Filter α} (θ : α → ℝ) (hθ : ∀ (a : α), 0 ≤ θ a) (ht : Filter.Tendsto θ l (nhds 0)) (u v : ↑unitInterval) : Filter.Tendsto (fun (a : α) => (Verification.nelsen19 (θ a) ⋯).cdf ![u, v]) l (nhds ((ProbabilityTheory.Copula.clayton 2 1 ⋯).cdf ![u, v]))

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

theorem Papers.AnsariRockel2024.nelsen19_schur_monotone {θ η : ℝ} (hθ : 0 ≤ θ) (hη : 0 ≤ η) (hθη : θ ≤ η) : (Verification.nelsen19 θ hθ).SchurBothLE (Verification.nelsen19 η hη)

theorem Papers.AnsariRockel2024.nelsen19_tendsto_atTop {α : Type u_1} {l : Filter α} (θ : α → ℝ) (hθ : ∀ (a : α), 0 ≤ θ a) (ht : Filter.Tendsto θ l Filter.atTop) (u v : ↑unitInterval) : Filter.Tendsto (fun (a : α) => (Verification.nelsen19 (θ a) ⋯).cdf ![u, v]) l (nhds ((ProbabilityTheory.Copula.comonotonic 2).cdf ![u, v]))

theorem Papers.AnsariRockel2024.nelsen19_toMeasure_density {θ : ℝ} (hθ : 0 < θ) : (Verification.nelsen19 θ ⋯).toMeasure = MeasureTheory.volume.withDensity fun (x : Fin 2 → ↑unitInterval) => ENNReal.ofReal (Verification.n19Density θ x)

theorem Papers.AnsariRockel2024.nelsen19_density_tp2 (θ : ℝ) (hθ : 0 ≤ θ) : (Verification.nelsen19 θ hθ).HasMTP2Density