← Mathematical handbook

Nelsen 22: trigonometric copula, exact CI/TP2 classification and tails

theorem Papers.AnsariRockel2024.nelsen22_zero : Verification.nelsen22 0 ⋯ = ProbabilityTheory.Copula.independence 2

theorem Papers.AnsariRockel2024.nelsen22_cdf_full {θ : ℝ} (hθ : 0 < θ) (hθ1 : θ ≤ 1) (u v : ↑unitInterval) : (Verification.nelsen22 θ ⋯).cdf ![u, v] = (1 - Real.sin (min (Real.arcsin (1 - ↑u ^ θ) + Real.arcsin (1 - ↑v ^ θ)) (Real.pi / 2))) ^ θ⁻¹

theorem Papers.AnsariRockel2024.nelsen22_cdf_printed {θ : ℝ} (hθ : 0 < θ) (hθ1 : θ ≤ 1) (u v : ↑unitInterval) : (Verification.nelsen22 θ ⋯).cdf ![u, v] = if -(Real.pi / 2) ≤ Real.arcsin (↑u ^ θ - 1) + Real.arcsin (↑v ^ θ - 1) then (1 + Real.sin (Real.arcsin (↑u ^ θ - 1) + Real.arcsin (↑v ^ θ - 1))) ^ θ⁻¹ else 0

theorem Papers.AnsariRockel2024.nelsen22_not_pqd {θ : ℝ} (hθ : 0 < θ) (hθ1 : θ ≤ 1) : ¬(Verification.nelsen22 θ ⋯).IsPQD

theorem Papers.AnsariRockel2024.nelsen22_isCI_iff (θ : ℝ) (hθ : θ ∈ Set.Icc 0 1) : (Verification.nelsen22 θ hθ).IsCI ↔ θ = 0

theorem Papers.AnsariRockel2024.nelsen22_density_tp2_iff (θ : ℝ) (hθ : θ ∈ Set.Icc 0 1) : (Verification.nelsen22 θ hθ).HasMTP2Density ↔ θ = 0

theorem Papers.AnsariRockel2024.nelsen22_lowerTail (θ : ℝ) (hθ : θ ∈ Set.Icc 0 1) : (Verification.nelsen22 θ hθ).HasLowerTailDependence 0

theorem Papers.AnsariRockel2024.nelsen22_upperTail (θ : ℝ) (hθ : θ ∈ Set.Icc 0 1) : (Verification.nelsen22 θ hθ).HasUpperTailDependence 0

theorem Papers.AnsariRockel2024.nelsen22_tendsto_zero {α : Type u_1} {l : Filter α} (θ : α → ℝ) (hθ : ∀ (a : α), θ a ∈ Set.Icc 0 1) (ht : Filter.Tendsto θ l (nhds 0)) (u v : ↑unitInterval) : Filter.Tendsto (fun (a : α) => (Verification.nelsen22 (θ a) ⋯).cdf ![u, v]) l (nhds ((ProbabilityTheory.Copula.independence 2).cdf ![u, v]))

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

theorem Papers.AnsariRockel2024.nelsen22_isCD (θ : ℝ) (hθ : θ ∈ Set.Icc 0 1) : (Verification.nelsen22 θ hθ).IsCD

theorem Papers.AnsariRockel2024.nelsen22_isNQD (θ : ℝ) (hθ : θ ∈ Set.Icc 0 1) : (Verification.nelsen22 θ hθ).IsNQD

theorem Papers.AnsariRockel2024.nelsen22_lowerOrthant_antitone {θ η : ℝ} (hθ : θ ∈ Set.Icc 0 1) (hη : η ∈ Set.Icc 0 1) (hθη : θ ≤ η) : (Verification.nelsen22 η hη).LowerOrthantLE (Verification.nelsen22 θ hθ)

theorem Papers.AnsariRockel2024.nelsen22_schur_monotone {θ η : ℝ} (hθ : θ ∈ Set.Icc 0 1) (hη : η ∈ Set.Icc 0 1) (hθη : θ ≤ η) : (Verification.nelsen22 θ hθ).SchurBothLE (Verification.nelsen22 η hη)