← Mathematical handbook

Tables 1–3: Nelsen 20 constructor, independence member, CI and tails

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

theorem Papers.AnsariRockel2024.nelsen20_zero : Verification.nelsen20 0 ⋯ = ProbabilityTheory.Copula.independence 2

theorem Papers.AnsariRockel2024.nelsen20_ci (θ : ℝ) (hθ : 0 ≤ θ) : (Verification.nelsen20 θ hθ).IsCI

theorem Papers.AnsariRockel2024.nelsen20_tails (θ : ℝ) (hθ : 0 ≤ θ) : (Verification.nelsen20 θ hθ).HasLowerTailDependence (if θ = 0 then 0 else 1) ∧ (Verification.nelsen20 θ hθ).HasUpperTailDependence 0

theorem Papers.AnsariRockel2024.nelsen20_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.nelsen20 (θ a) ⋯).cdf ![u, v]) l (nhds ((ProbabilityTheory.Copula.independence 2).cdf ![u, v]))

theorem Papers.AnsariRockel2024.nelsen20_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.nelsen20 (θ a) ⋯).cdf ![u, v]) l (nhds ((ProbabilityTheory.Copula.comonotonic 2).cdf ![u, v]))

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

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

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

theorem Papers.AnsariRockel2024.nelsen20_density_tp2 (θ : ℝ) (hθ : 0 ≤ θ) : (Verification.nelsen20 θ hθ).HasMTP2Density