theorem
Papers.AnsariRockel2024.bb5_limit_comonotonic
{ι : Type u_1}
{l : Filter ι}
(θ : ℝ)
(hθ : 1 ≤ θ)
(δ : ι → ℝ)
(hδ : ∀ (i : ι), 0 < δ i)
(hd : Filter.Tendsto δ l Filter.atTop)
(u : Fin 2 → ↑unitInterval)
:
Filter.Tendsto (fun (i : ι) => (Verification.bb5 θ (δ i) hθ ⋯).cdf u) l
(nhds ((ProbabilityTheory.Copula.comonotonic 2).cdf u))
theorem
Papers.AnsariRockel2024.bb5_limit_gumbel_interior
{ι : Type u_1}
{l : Filter ι}
(θ : ℝ)
(hθ : 1 ≤ θ)
(δ : ι → ℝ)
(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.bb5 θ (δ i) hθ ⋯).cdf ![u, v]) l
(nhds ((ProbabilityTheory.Copula.gumbel θ hθ).cdf ![u, v]))
theorem
Papers.AnsariRockel2024.bb5_limit_gumbel
{ι : Type u_1}
{l : Filter ι}
(θ : ℝ)
(hθ : 1 ≤ θ)
(δ : ι → ℝ)
(hδ : ∀ (i : ι), 0 < δ i)
(hd : Filter.Tendsto δ l (nhds 0))
(u : Fin 2 → ↑unitInterval)
:
Filter.Tendsto (fun (i : ι) => (Verification.bb5 θ (δ i) hθ ⋯).cdf u) l
(nhds ((ProbabilityTheory.Copula.gumbel θ hθ).cdf u))
theorem
Papers.AnsariRockel2024.bb5_limit_comonotonic_uniform
{ι : Type u_1}
{l : Filter ι}
(θ : ℝ)
(hθ : 1 ≤ θ)
(δ : ι → ℝ)
(hδ : ∀ (i : ι), 0 < δ i)
(hd : Filter.Tendsto δ l Filter.atTop)
:
TendstoUniformly (fun (i : ι) => (Verification.bb5 θ (δ i) hθ ⋯).cdf) (ProbabilityTheory.Copula.comonotonic 2).cdf l
theorem
Papers.AnsariRockel2024.bb5_limit_gumbel_uniform
{ι : Type u_1}
{l : Filter ι}
(θ : ℝ)
(hθ : 1 ≤ θ)
(δ : ι → ℝ)
(hδ : ∀ (i : ι), 0 < δ i)
(hd : Filter.Tendsto δ l (nhds 0))
:
TendstoUniformly (fun (i : ι) => (Verification.bb5 θ (δ i) hθ ⋯).cdf) (ProbabilityTheory.Copula.gumbel θ hθ).cdf l