← Mathematical handbook

Nelsen 18: constructor, CDF, tails and conditional classifications

theorem Papers.AnsariRockel2024.nelsen18_cdf_full (θ : ℝ) (hθ : 2 ≤ θ) (u v : ↑unitInterval) : (Verification.nelsen18 θ hθ).cdf ![u, v] = max 0 (1 + θ / Real.log (Verification.n18Inv θ u + Verification.n18Inv θ v))

theorem Papers.AnsariRockel2024.nelsen18_cdf_of_lt_one (θ : ℝ) (hθ : 2 ≤ θ) (u v : ↑unitInterval) (hu : u < 1) (hv : v < 1) : (Verification.nelsen18 θ hθ).cdf ![u, v] = max 0 (1 + θ / Real.log (Real.exp (θ / (↑u - 1)) + Real.exp (θ / (↑v - 1))))

theorem Papers.AnsariRockel2024.nelsen18_lowerTail (θ : ℝ) (hθ : 2 ≤ θ) : (Verification.nelsen18 θ hθ).HasLowerTailDependence 0

theorem Papers.AnsariRockel2024.nelsen18_upperTail (θ : ℝ) (hθ : 2 ≤ θ) : (Verification.nelsen18 θ hθ).HasUpperTailDependence 1

theorem Papers.AnsariRockel2024.nelsen18_not_pqd (θ : ℝ) (hθ : 2 ≤ θ) : ¬(Verification.nelsen18 θ hθ).IsPQD

theorem Papers.AnsariRockel2024.nelsen18_not_ci (θ : ℝ) (hθ : 2 ≤ θ) : ¬(Verification.nelsen18 θ hθ).IsCI

theorem Papers.AnsariRockel2024.nelsen18_not_density_tp2 (θ : ℝ) (hθ : 2 ≤ θ) : ¬(Verification.nelsen18 θ hθ).HasMTP2Density

theorem Papers.AnsariRockel2024.nelsen18_not_nqd (θ : ℝ) (hθ : 2 ≤ θ) : ¬(Verification.nelsen18 θ hθ).IsNQD

theorem Papers.AnsariRockel2024.nelsen18_not_cd (θ : ℝ) (hθ : 2 ≤ θ) : ¬(Verification.nelsen18 θ hθ).IsCD

theorem Papers.AnsariRockel2024.nelsen18_lowerOrthant_monotone {θ η : ℝ} (hθ : 2 ≤ θ) (hθη : θ ≤ η) : (Verification.nelsen18 θ hθ).LowerOrthantLE (Verification.nelsen18 η ⋯)

theorem Papers.AnsariRockel2024.nelsen18_tendsto_parameter {α : Type u_1} {l : Filter α} (θ : α → ℝ) (hθ : ∀ (a : α), 2 ≤ θ a) {η : ℝ} (hη : 2 ≤ η) (ht : Filter.Tendsto θ l (nhds η)) (u v : ↑unitInterval) : Filter.Tendsto (fun (a : α) => (Verification.nelsen18 (θ a) ⋯).cdf ![u, v]) l (nhds ((Verification.nelsen18 η hη).cdf ![u, v]))

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