Infinite-parameter endpoints for Nelsen 14 and Genest–Ghoudi from Table 2 #
theorem
Papers.AnsariRockel2024.nelsen14_tendsto_atTop
{α : Type u_1}
{l : Filter α}
(θ : α → ℝ)
(hθ : ∀ (z : α), 1 ≤ θ z)
(hlim : Filter.Tendsto θ l Filter.atTop)
(u : Fin 2 → ↑unitInterval)
:
Filter.Tendsto (fun (z : α) => (ProbabilityTheory.Copula.nelsen14 (θ z) ⋯).cdf u) l
(nhds ((ProbabilityTheory.Copula.comonotonic 2).cdf u))
Nelsen 14 tends pointwise to comonotonicity on the full closed square.
theorem
Papers.AnsariRockel2024.genestGhoudi_tendsto_atTop
{α : Type u_1}
{l : Filter α}
(θ : α → ℝ)
(hθ : ∀ (z : α), 1 ≤ θ z)
(hlim : Filter.Tendsto θ l Filter.atTop)
(u : Fin 2 → ↑unitInterval)
:
Filter.Tendsto (fun (z : α) => (ProbabilityTheory.Copula.genestGhoudi (θ z) ⋯).cdf u) l
(nhds ((ProbabilityTheory.Copula.comonotonic 2).cdf u))
Genest–Ghoudi tends pointwise to comonotonicity on the full closed square.