Documentation

Papers.AnsariRockel2024.Nelsen10

← Mathematical handbook

Tables 1–3: Nelsen 10, its actual CDF, endpoints and dependence exclusions #

source
theorem Papers.AnsariRockel2024.nelsen10_cdf (θ u v : ↑unitInterval) (hθ : 0 < ↑θ) :
(Verification.nelsen10 θ).cdf ![u, v] = ↑u * ↑v / (1 + (1 - ↑u ^ ↑θ) * (1 - ↑v ^ ↑θ)) ^ (↑θ)⁻¹
source
theorem Papers.AnsariRockel2024.nelsen10_zero :
Verification.nelsen10 0 = ProbabilityTheory.Copula.independence 2
source
theorem Papers.AnsariRockel2024.nelsen10_one :
Verification.nelsen10 1 = ProbabilityTheory.Copula.amh (-1) ⋯ ⋯
source
theorem Papers.AnsariRockel2024.nelsen10_nqd (θ : ↑unitInterval) :
(Verification.nelsen10 θ).IsNQD
source
theorem Papers.AnsariRockel2024.nelsen10_pqd_iff (θ : ↑unitInterval) :
(Verification.nelsen10 θ).IsPQD ↔ θ = 0
source
theorem Papers.AnsariRockel2024.nelsen10_ci_iff (θ : ↑unitInterval) :
(Verification.nelsen10 θ).IsCI ↔ θ = 0
source
theorem Papers.AnsariRockel2024.nelsen10_density_tp2_iff (θ : ↑unitInterval) :
(Verification.nelsen10 θ).HasMTP2Density ↔ θ = 0
source
theorem Papers.AnsariRockel2024.nelsen10_tails (θ : ↑unitInterval) :
(Verification.nelsen10 θ).HasLowerTailDependence 0 ∧ (Verification.nelsen10 θ).HasUpperTailDependence 0
source
theorem Papers.AnsariRockel2024.nelsen10_cd (θ : ↑unitInterval) :
(Verification.nelsen10 θ).IsCD
source
theorem Papers.AnsariRockel2024.nelsen10_continuousAt_zero (u v : ↑unitInterval) :
ContinuousAt (fun (θ : ↑unitInterval) => (Verification.nelsen10 θ).cdf ![u, v]) 0
source
theorem Papers.AnsariRockel2024.nelsen10_cdf_crossing :
(Verification.nelsen10 Verification.n10Half).cdf ![Verification.n10Low, Verification.n10Low] < (Verification.nelsen10 1).cdf ![Verification.n10Low, Verification.n10Low] ∧ (Verification.nelsen10 1).cdf ![Verification.n10High, Verification.n10High] < (Verification.nelsen10 Verification.n10Half).cdf ![Verification.n10High, Verification.n10High]
source
theorem Papers.AnsariRockel2024.nelsen10_orthant_incomparable :
¬(Verification.nelsen10 Verification.n10Half).LowerOrthantLE (Verification.nelsen10 1) ∧ ¬(Verification.nelsen10 1).LowerOrthantLE (Verification.nelsen10 Verification.n10Half)
source
theorem Papers.AnsariRockel2024.nelsen10_schur_incomparable :
¬(Verification.nelsen10 Verification.n10Half).SchurLE (Verification.nelsen10 1) ∧ ¬(Verification.nelsen10 1).SchurLE (Verification.nelsen10 Verification.n10Half)
source
theorem Papers.AnsariRockel2024.nelsen10_schurBoth_incomparable :
¬(Verification.nelsen10 Verification.n10Half).SchurBothLE (Verification.nelsen10 1) ∧ ¬(Verification.nelsen10 1).SchurBothLE (Verification.nelsen10 Verification.n10Half)