← Mathematical handbook

noncomputable def Verification.joeExtremeValue (δ : ℝ) (hδ : 0 < δ) (α β : ↑unitInterval) : ProbabilityTheory.Copula 2

Equations

• Verification.joeExtremeValue δ hδ α β = (Verification.galambos δ hδ).maxProduct (ProbabilityTheory.Copula.independence 2) ![α, β]

theorem Papers.AnsariRockel2024.joeExtremeValue_isExtremeValue (δ : ℝ) (hδ : 0 < δ) (α β : ↑unitInterval) : (Verification.joeExtremeValue δ hδ α β).IsExtremeValue

theorem Papers.AnsariRockel2024.joeExtremeValue_isCI (δ : ℝ) (hδ : 0 < δ) (α β : ↑unitInterval) : (Verification.joeExtremeValue δ hδ α β).IsCI

theorem Papers.AnsariRockel2024.joeExtremeValue_cdf_product (δ : ℝ) (hδ : 0 < δ) (α β u v : ↑unitInterval) : (Verification.joeExtremeValue δ hδ α β).cdf ![u, v] = (Verification.galambos δ hδ).cdf ![ProbabilityTheory.Copula.unitPower u ↑α ⋯, ProbabilityTheory.Copula.unitPower v ↑β ⋯] * (↑u ^ (1 - ↑α) * ↑v ^ (1 - ↑β))

theorem Papers.AnsariRockel2024.joeExtremeValue_cdf_interior (δ : ℝ) (hδ : 0 < δ) (α β u v : ↑unitInterval) (hα : 0 < ↑α) (hβ : 0 < ↑β) (hu : ↑u ∈ Set.Ioo 0 1) (hv : ↑v ∈ Set.Ioo 0 1) : (Verification.joeExtremeValue δ hδ α β).cdf ![u, v] = ↑u * ↑v * Real.exp (((↑α * -Real.log ↑u) ^ (-δ) + (↑β * -Real.log ↑v) ^ (-δ)) ^ (-1 / δ))

theorem Papers.AnsariRockel2024.joeExtremeValue_unit_weights (δ : ℝ) (hδ : 0 < δ) : Verification.joeExtremeValue δ hδ 1 1 = Verification.galambos δ hδ

theorem Papers.AnsariRockel2024.joeExtremeValue_zero_weight (δ : ℝ) (hδ : 0 < δ) (α β : ↑unitInterval) (h : α = 0 ∨ β = 0) : Verification.joeExtremeValue δ hδ α β = ProbabilityTheory.Copula.independence 2