theorem
Papers.AnsariRockel2024.huslerReiss_limit_comonotonic
{ι : Type u_1}
{l : Filter ι}
(δ : ι → ℝ)
(hδ : ∀ (i : ι), 0 < δ i)
(hd : Filter.Tendsto δ l Filter.atTop)
(u : Fin 2 → ↑unitInterval)
:
Filter.Tendsto (fun (i : ι) => (Verification.huslerReissPositive (δ i) ⋯).cdf u) l
(nhds ((ProbabilityTheory.Copula.comonotonic 2).cdf u))
theorem
Papers.AnsariRockel2024.huslerReiss_limit_independence_interior
{ι : Type u_1}
{l : Filter ι}
(δ : ι → ℝ)
(hδ : ∀ (i : ι), 0 < δ i)
(hd : Filter.Tendsto δ l (nhds 0))
(u v : ↑unitInterval)
(hu : ↑u ∈ Set.Ioo 0 1)
(hv : ↑v ∈ Set.Ioo 0 1)
:
Filter.Tendsto (fun (i : ι) => (Verification.huslerReissPositive (δ i) ⋯).cdf ![u, v]) l (nhds (↑u * ↑v))
theorem
Papers.AnsariRockel2024.huslerReiss_limit_independence
{ι : Type u_1}
{l : Filter ι}
(δ : ι → ℝ)
(hδ : ∀ (i : ι), 0 < δ i)
(hd : Filter.Tendsto δ l (nhds 0))
(u : Fin 2 → ↑unitInterval)
:
Filter.Tendsto (fun (i : ι) => (Verification.huslerReissPositive (δ i) ⋯).cdf u) l
(nhds ((ProbabilityTheory.Copula.independence 2).cdf u))
theorem
Papers.AnsariRockel2024.huslerReiss_limit_comonotonic_uniform
{ι : Type u_1}
{l : Filter ι}
(δ : ι → ℝ)
(hδ : ∀ (i : ι), 0 < δ i)
(hd : Filter.Tendsto δ l Filter.atTop)
:
TendstoUniformly (fun (i : ι) => (Verification.huslerReissPositive (δ i) ⋯).cdf)
(ProbabilityTheory.Copula.comonotonic 2).cdf l
theorem
Papers.AnsariRockel2024.huslerReiss_limit_independence_uniform
{ι : Type u_1}
{l : Filter ι}
(δ : ι → ℝ)
(hδ : ∀ (i : ι), 0 < δ i)
(hd : Filter.Tendsto δ l (nhds 0))
:
TendstoUniformly (fun (i : ι) => (Verification.huslerReissPositive (δ i) ⋯).cdf)
(ProbabilityTheory.Copula.independence 2).cdf l