← Mathematical handbook

Tables 1–2: Nelsen 17 on both nonzero parameter branches

theorem Papers.AnsariRockel2024.nelsen17_cdf_full (θ : ℝ) (hθ : θ ≠ 0) (u v : ↑unitInterval) : (Verification.nelsen17 θ hθ).cdf ![u, v] = (1 + ((1 + ↑u) ^ (-θ) - 1) * ((1 + ↑v) ^ (-θ) - 1) / (2 ^ (-θ) - 1)) ^ (-θ⁻¹) - 1

theorem Papers.AnsariRockel2024.nelsen17_neg_one : Verification.nelsen17 (-1) ⋯ = ProbabilityTheory.Copula.independence 2

theorem Papers.AnsariRockel2024.nelsen17_isCI (θ : ℝ) (hθ : θ ≠ 0) (hθ1 : -1 ≤ θ) : (Verification.nelsen17 θ hθ).IsCI

theorem Papers.AnsariRockel2024.nelsen17_isCD (θ : ℝ) (hθ : θ ≠ 0) (hθ1 : θ ≤ -1) : (Verification.nelsen17 θ hθ).IsCD

theorem Papers.AnsariRockel2024.nelsen17_tails (θ : ℝ) (hθ : θ ≠ 0) : (Verification.nelsen17 θ hθ).HasLowerTailDependence 0 ∧ (Verification.nelsen17 θ hθ).HasUpperTailDependence 0

theorem Papers.AnsariRockel2024.nelsen17_isCI_iff (θ : ℝ) (hθ : θ ≠ 0) : (Verification.nelsen17 θ hθ).IsCI ↔ -1 ≤ θ

theorem Papers.AnsariRockel2024.nelsen17_isCD_iff (θ : ℝ) (hθ : θ ≠ 0) : (Verification.nelsen17 θ hθ).IsCD ↔ θ ≤ -1

theorem Papers.AnsariRockel2024.nelsen17_isPQD_iff (θ : ℝ) (hθ : θ ≠ 0) : (Verification.nelsen17 θ hθ).IsPQD ↔ -1 ≤ θ

theorem Papers.AnsariRockel2024.nelsen17_isNQD_iff (θ : ℝ) (hθ : θ ≠ 0) : (Verification.nelsen17 θ hθ).IsNQD ↔ θ ≤ -1

theorem Papers.AnsariRockel2024.nelsen17_toMeasure_density (θ : ℝ) (hθ : θ ≠ 0) : (Verification.nelsen17 θ hθ).toMeasure = MeasureTheory.volume.withDensity fun (x : Fin 2 → ↑unitInterval) => ENNReal.ofReal (Verification.n17Density (-θ) x)

theorem Papers.AnsariRockel2024.nelsen17_density_tp2_iff (θ : ℝ) (hθ : θ ≠ 0) : (Verification.nelsen17 θ hθ).HasMTP2Density ↔ -1 ≤ θ

theorem Papers.AnsariRockel2024.nelsen17_lowerOrthant_monotone {θ η : ℝ} (hθ : θ ≠ 0) (hη : η ≠ 0) (hθη : θ ≤ η) : (Verification.nelsen17 θ hθ).LowerOrthantLE (Verification.nelsen17 η hη)

theorem Papers.AnsariRockel2024.nelsen17_schur_monotone {θ η : ℝ} (hθ : θ ≠ 0) (hη : η ≠ 0) (hθ1 : -1 ≤ θ) (hθη : θ ≤ η) : (Verification.nelsen17 θ hθ).SchurBothLE (Verification.nelsen17 η hη)

theorem Papers.AnsariRockel2024.nelsen17_schur_antitone {θ η : ℝ} (hθ : θ ≠ 0) (hη : η ≠ 0) (hη1 : η ≤ -1) (hθη : θ ≤ η) : (Verification.nelsen17 η hη).SchurBothLE (Verification.nelsen17 θ hθ)

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

theorem Papers.AnsariRockel2024.nelsen17_tendsto_zero {α : Type u_1} {l : Filter α} (θ : α → ℝ) (hθ : ∀ (a : α), θ a ≠ 0) (ht : Filter.Tendsto θ l (nhds 0)) (u v : ↑unitInterval) : Filter.Tendsto (fun (a : α) => (Verification.nelsen17 (θ a) ⋯).cdf ![u, v]) l (nhds (Real.exp (Real.log (1 + ↑u) * Real.log (1 + ↑v) / Real.log 2) - 1))

theorem Papers.AnsariRockel2024.nelsen17_tendsto_atBot {α : Type u_1} {l : Filter α} (θ : α → ℝ) (hθ : ∀ (a : α), θ a ≠ 0) (ht : Filter.Tendsto θ l Filter.atBot) (u v : ↑unitInterval) : Filter.Tendsto (fun (a : α) => (Verification.nelsen17 (θ a) ⋯).cdf ![u, v]) l (nhds (max 1 ((1 + ↑u) * (1 + ↑v) / 2) - 1))