← Mathematical handbook

Nelsen 21: measure constructor, printed CDF, and countermonotonic endpoint

theorem Papers.AnsariRockel2024.nelsen21_cdf_full (θ : ℝ) (hθ : 1 ≤ θ) (u v : ↑unitInterval) : (Verification.nelsen21 θ hθ).cdf ![u, v] = 1 - (1 - max 0 ((1 - (1 - ↑u) ^ θ) ^ θ⁻¹ + (1 - (1 - ↑v) ^ θ) ^ θ⁻¹ - 1) ^ θ) ^ θ⁻¹

theorem Papers.AnsariRockel2024.nelsen21_one : Verification.nelsen21 1 ⋯ = ProbabilityTheory.Copula.countermonotonic

theorem Papers.AnsariRockel2024.nelsen21_lowerTail (θ : ℝ) (hθ : 1 ≤ θ) : (Verification.nelsen21 θ hθ).HasLowerTailDependence 0

theorem Papers.AnsariRockel2024.nelsen21_upperTail (θ : ℝ) (hθ : 1 ≤ θ) : (Verification.nelsen21 θ hθ).HasUpperTailDependence (2 - 2 ^ θ⁻¹)

theorem Papers.AnsariRockel2024.nelsen21_not_pqd (θ : ℝ) (hθ : 1 ≤ θ) : ¬(Verification.nelsen21 θ hθ).IsPQD

theorem Papers.AnsariRockel2024.nelsen21_not_ci (θ : ℝ) (hθ : 1 ≤ θ) : ¬(Verification.nelsen21 θ hθ).IsCI

theorem Papers.AnsariRockel2024.nelsen21_not_density_tp2 (θ : ℝ) (hθ : 1 ≤ θ) : ¬(Verification.nelsen21 θ hθ).HasMTP2Density

theorem Papers.AnsariRockel2024.nelsen21_isCD_iff (θ : ℝ) (hθ : 1 ≤ θ) : (Verification.nelsen21 θ hθ).IsCD ↔ θ = 1

theorem Papers.AnsariRockel2024.nelsen21_isNQD_iff (θ : ℝ) (hθ : 1 ≤ θ) : (Verification.nelsen21 θ hθ).IsNQD ↔ θ = 1

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

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

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

theorem Papers.AnsariRockel2024.nelsen21_lowerOrthant_monotone {θ η : ℝ} (hθ : 1 ≤ θ) (hθη : θ ≤ η) : (Verification.nelsen21 θ hθ).LowerOrthantLE (Verification.nelsen21 η ⋯)

theorem Papers.AnsariRockel2024.nelsen21_not_schur_monotone : ¬∀ (θ η : ℝ) (hθ : 1 ≤ θ) (hθη : θ ≤ η), (Verification.nelsen21 θ hθ).SchurLE (Verification.nelsen21 η ⋯)

theorem Papers.AnsariRockel2024.nelsen21_not_schur_antitone : ¬∀ (θ η : ℝ) (hθ : 1 ≤ θ) (hθη : θ ≤ η), (Verification.nelsen21 η ⋯).SchurLE (Verification.nelsen21 θ hθ)