theorem
Papers.AnsariRockel2024.joeExtremeValue_lowerOrthant_mono
(δ ε : ℝ)
(hδ : 0 < δ)
(hε : 0 < ε)
(hδε : δ ≤ ε)
(α β : ↑unitInterval)
:
(Verification.joeExtremeValue δ hδ α β).LowerOrthantLE (Verification.joeExtremeValue ε hε α β)
theorem
Papers.AnsariRockel2024.joeExtremeValue_schurBoth_mono
(δ ε : ℝ)
(hδ : 0 < δ)
(hε : 0 < ε)
(hδε : δ ≤ ε)
(α β : ↑unitInterval)
:
(Verification.joeExtremeValue δ hδ α β).SchurBothLE (Verification.joeExtremeValue ε hε α β)
theorem
Papers.AnsariRockel2024.joeExtremeValue_limit_marshallOlkin
{ι : Type u_1}
{l : Filter ι}
(δ : ι → ℝ)
(hδ : ∀ (i : ι), 0 < δ i)
(hd : Filter.Tendsto δ l Filter.atTop)
(α β : ↑unitInterval)
(u : Fin 2 → ↑unitInterval)
:
Filter.Tendsto (fun (i : ι) => (Verification.joeExtremeValue (δ i) ⋯ α β).cdf u) l
(nhds ((ProbabilityTheory.Copula.marshallOlkin α β).cdf u))
theorem
Papers.AnsariRockel2024.joeExtremeValue_limit_independence
{ι : Type u_1}
{l : Filter ι}
(δ : ι → ℝ)
(hδ : ∀ (i : ι), 0 < δ i)
(hd : Filter.Tendsto δ l (nhds 0))
(α β : ↑unitInterval)
(u : Fin 2 → ↑unitInterval)
:
Filter.Tendsto (fun (i : ι) => (Verification.joeExtremeValue (δ i) ⋯ α β).cdf u) l
(nhds ((ProbabilityTheory.Copula.independence 2).cdf u))