Documentation

Papers.AnsariRockel2024.GumbelBarnett

← Mathematical handbook

Tables 1–3: Gumbel–Barnett on its full closed parameter interval #

source
theorem Papers.AnsariRockel2024.gumbelBarnett_cdf (θ u v : ↑unitInterval) :
(Verification.gumbelBarnett θ).cdf ![u, v] = ↑u * ↑v * Real.exp (-↑θ * Real.log ↑u * Real.log ↑v)
source
theorem Papers.AnsariRockel2024.gumbelBarnett_zero :
Verification.gumbelBarnett 0 = ProbabilityTheory.Copula.independence 2
source
theorem Papers.AnsariRockel2024.gumbelBarnett_parameter_continuous (u v : ↑unitInterval) :
Continuous fun (θ : ↑unitInterval) => (Verification.gumbelBarnett θ).cdf ![u, v]
source
theorem Papers.AnsariRockel2024.gumbelBarnett_cd (θ : ↑unitInterval) :
(Verification.gumbelBarnett θ).IsCD
source
theorem Papers.AnsariRockel2024.gumbelBarnett_ci_iff (θ : ↑unitInterval) :
(Verification.gumbelBarnett θ).IsCI ↔ θ = 0
source
theorem Papers.AnsariRockel2024.gumbelBarnett_density_tp2_iff (θ : ↑unitInterval) :
(Verification.gumbelBarnett θ).HasMTP2Density ↔ θ = 0
source
theorem Papers.AnsariRockel2024.gumbelBarnett_lowerOrthant_iff (θ η : ↑unitInterval) :
(Verification.gumbelBarnett θ).LowerOrthantLE (Verification.gumbelBarnett η) ↔ η ≤ θ
source
theorem Papers.AnsariRockel2024.gumbelBarnett_schur_iff (θ η : ↑unitInterval) :
(Verification.gumbelBarnett θ).SchurBothLE (Verification.gumbelBarnett η) ↔ θ ≤ η
source
theorem Papers.AnsariRockel2024.gumbelBarnett_tails (θ : ↑unitInterval) :
(Verification.gumbelBarnett θ).HasLowerTailDependence 0 ∧ (Verification.gumbelBarnett θ).HasUpperTailDependence 0
source
theorem Papers.AnsariRockel2024.gumbelBarnett_conditionalCDF (θ v : ↑unitInterval) :
(fun (u : ↑unitInterval) => (Verification.gumbelBarnett θ).conditionalCDF u v) =ᵐ[MeasureTheory.volume] fun (u : ↑unitInterval) => Verification.gbConditional θ u v
source
theorem Papers.AnsariRockel2024.gumbelBarnett_xi (θ : ↑unitInterval) (hθ : 0 < ↑θ) :
(Verification.gumbelBarnett θ).chatterjeeXi = 3 * Real.exp (3 / (2 * ↑θ)) / (4 * ↑θ) * Verification.exponentialIntegralE1 (3 / (2 * ↑θ)) + ↑θ / 3 - 1 / 2
source
theorem Papers.AnsariRockel2024.gumbelBarnett_xi_zero :
(Verification.gumbelBarnett 0).chatterjeeXi = 0