theorem
Papers.AnsariRockel2024.galambos_limit_independence_uniform
{ι : Type u_1}
{l : Filter ι}
(δ : ι → ℝ)
(hδ : ∀ (i : ι), 0 < δ i)
(hd : Filter.Tendsto δ l (nhds 0))
:
TendstoUniformly (fun (i : ι) => (Verification.galambos (δ i) ⋯).cdf) (ProbabilityTheory.Copula.independence 2).cdf l
theorem
Papers.AnsariRockel2024.galambos_limit_comonotonic_uniform
{ι : Type u_1}
{l : Filter ι}
(δ : ι → ℝ)
(hδ : ∀ (i : ι), 0 < δ i)
(hd : Filter.Tendsto δ l Filter.atTop)
:
TendstoUniformly (fun (i : ι) => (Verification.galambos (δ i) ⋯).cdf) (ProbabilityTheory.Copula.comonotonic 2).cdf l
theorem
Papers.AnsariRockel2024.joeExtremeValue_limit_independence_uniform
{ι : Type u_1}
{l : Filter ι}
(δ : ι → ℝ)
(hδ : ∀ (i : ι), 0 < δ i)
(hd : Filter.Tendsto δ l (nhds 0))
(α β : ↑unitInterval)
:
TendstoUniformly (fun (i : ι) => (Verification.joeExtremeValue (δ i) ⋯ α β).cdf)
(ProbabilityTheory.Copula.independence 2).cdf l
theorem
Papers.AnsariRockel2024.joeExtremeValue_limit_marshallOlkin_uniform
{ι : Type u_1}
{l : Filter ι}
(δ : ι → ℝ)
(hδ : ∀ (i : ι), 0 < δ i)
(hd : Filter.Tendsto δ l Filter.atTop)
(α β : ↑unitInterval)
:
TendstoUniformly (fun (i : ι) => (Verification.joeExtremeValue (δ i) ⋯ α β).cdf)
(ProbabilityTheory.Copula.marshallOlkin α β).cdf l