← Mathematical handbook

Tables 1–3: Nelsen 11 as an actual copula measure

theorem Papers.AnsariRockel2024.nelsen11_cdf (θ : ℝ) (hθ : 0 < θ) (hθ1 : θ ≤ 1 / 2) (u v : ↑unitInterval) : (Verification.nelsen11 θ ⋯ hθ1).cdf ![u, v] = max 0 (↑u ^ θ * ↑v ^ θ - 2 * (1 - ↑u ^ θ) * (1 - ↑v ^ θ)) ^ θ⁻¹

theorem Papers.AnsariRockel2024.nelsen11_zero : Verification.nelsen11 0 ⋯ ⋯ = ProbabilityTheory.Copula.independence 2

theorem Papers.AnsariRockel2024.nelsen11_nqd (θ : ℝ) (hθ0 : 0 ≤ θ) (hθ1 : θ ≤ 1 / 2) : (Verification.nelsen11 θ hθ0 hθ1).IsNQD

theorem Papers.AnsariRockel2024.nelsen11_pqd_iff (θ : ℝ) (hθ0 : 0 ≤ θ) (hθ1 : θ ≤ 1 / 2) : (Verification.nelsen11 θ hθ0 hθ1).IsPQD ↔ θ = 0

theorem Papers.AnsariRockel2024.nelsen11_ci_iff (θ : ℝ) (hθ0 : 0 ≤ θ) (hθ1 : θ ≤ 1 / 2) : (Verification.nelsen11 θ hθ0 hθ1).IsCI ↔ θ = 0

theorem Papers.AnsariRockel2024.nelsen11_density_tp2_iff (θ : ℝ) (hθ0 : 0 ≤ θ) (hθ1 : θ ≤ 1 / 2) : (Verification.nelsen11 θ hθ0 hθ1).HasMTP2Density ↔ θ = 0

theorem Papers.AnsariRockel2024.nelsen11_tails (θ : ℝ) (hθ0 : 0 ≤ θ) (hθ1 : θ ≤ 1 / 2) : (Verification.nelsen11 θ hθ0 hθ1).HasLowerTailDependence 0 ∧ (Verification.nelsen11 θ hθ0 hθ1).HasUpperTailDependence 0

theorem Papers.AnsariRockel2024.nelsen11_tendsto_zero {α : Type u_1} {l : Filter α} (θ : α → ℝ) (hθ0 : ∀ (z : α), 0 ≤ θ z) (hθ1 : ∀ (z : α), θ z ≤ 1 / 2) (hlim : Filter.Tendsto θ l (nhds 0)) (u v : ↑unitInterval) : Filter.Tendsto (fun (z : α) => (Verification.nelsen11 (θ z) ⋯ ⋯).cdf ![u, v]) l (nhds ((ProbabilityTheory.Copula.independence 2).cdf ![u, v]))

theorem Papers.AnsariRockel2024.nelsen11_cd (θ : ℝ) (hθ0 : 0 ≤ θ) (hθ1 : θ ≤ 1 / 2) : (Verification.nelsen11 θ hθ0 hθ1).IsCD

theorem Papers.AnsariRockel2024.nelsen11_lowerOrthant_antitone {θ η : ℝ} (hθ0 : 0 ≤ θ) (hθ1 : θ ≤ 1 / 2) (hη0 : 0 ≤ η) (hη1 : η ≤ 1 / 2) (hθη : θ ≤ η) : (Verification.nelsen11 η hη0 hη1).LowerOrthantLE (Verification.nelsen11 θ hθ0 hθ1)

theorem Papers.AnsariRockel2024.nelsen11_schur_monotone {θ η : ℝ} (hθ0 : 0 ≤ θ) (hθ1 : θ ≤ 1 / 2) (hη0 : 0 ≤ η) (hη1 : η ≤ 1 / 2) (hθη : θ ≤ η) : (Verification.nelsen11 θ hθ0 hθ1).SchurBothLE (Verification.nelsen11 η hη0 hη1)