← Mathematical handbook

Tables 1–2: Nelsen 16 constructor and zero endpoint

theorem Papers.AnsariRockel2024.nelsen16_cdf_full (θ : ℝ) (hθ : 0 ≤ θ) (u v : ↑unitInterval) : (Verification.nelsen16 θ hθ).cdf ![u, v] = if u = 0 ∨ v = 0 then 0 else have s := ↑u + ↑v - 1 - θ * ((↑u)⁻¹ + (↑v)⁻¹ - 1); (s + √(s ^ 2 + 4 * θ)) / 2

theorem Papers.AnsariRockel2024.nelsen16_zero : Verification.nelsen16 0 ⋯ = ProbabilityTheory.Copula.countermonotonic

theorem Papers.AnsariRockel2024.nelsen16_cdf_continuous_parameter (u v : ↑unitInterval) : Continuous fun (θ : ↑(Set.Ici 0)) => (Verification.nelsen16 ↑θ ⋯).cdf ![u, v]

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

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

theorem Papers.AnsariRockel2024.nelsen16_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.nelsen16 (θ z) ⋯).cdf ![u, v]) l (nhds ((ProbabilityTheory.Copula.clayton 2 1 ⋯).cdf ![u, v]))

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

theorem Papers.AnsariRockel2024.nelsen16_ci {θ : ℝ} (hθ : 3 ≤ θ) : (Verification.nelsen16 θ ⋯).IsCI

theorem Papers.AnsariRockel2024.nelsen16_schur_monotone {θ η : ℝ} (hθ : 3 ≤ θ) (hη : 3 ≤ η) (hθη : θ ≤ η) : (Verification.nelsen16 θ ⋯).SchurBothLE (Verification.nelsen16 η ⋯)

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

theorem Papers.AnsariRockel2024.nelsen16_density_tp2 {θ : ℝ} (hθ : 3 + 2 * √2 ≤ θ) : (Verification.nelsen16 θ ⋯).HasMTP2Density

theorem Papers.AnsariRockel2024.nelsen16_ci_iff (θ : ℝ) (hθ : 0 ≤ θ) : (Verification.nelsen16 θ hθ).IsCI ↔ 3 ≤ θ

theorem Papers.AnsariRockel2024.nelsen16_density_tp2_iff (θ : ℝ) (hθ : 0 ≤ θ) : (Verification.nelsen16 θ hθ).HasMTP2Density ↔ 3 + 2 * √2 ≤ θ