Infinite-parameter limits for Nelsen 14 and Genest–Ghoudi #
The reciprocal-parameter power expansion and a variable-input two-coordinate power-norm squeeze yield full-square pointwise convergence to comonotonicity.
theorem
ProbabilityTheory.Copula.tendsto_nelsen14_atTop
{α : Type u_1}
{l : Filter α}
(θ : α → ℝ)
(hθ : ∀ (z : α), 1 ≤ θ z)
(hlim : Filter.Tendsto θ l Filter.atTop)
(u : Fin 2 → ↑unitInterval)
:
Filter.Tendsto (fun (z : α) => (nelsen14 (θ z) ⋯).cdf u) l (nhds ((comonotonic 2).cdf u))
Nelsen 14 converges pointwise to the upper Fréchet bound on the closed square.
theorem
ProbabilityTheory.Copula.tendsto_genestGhoudi_atTop
{α : Type u_1}
{l : Filter α}
(θ : α → ℝ)
(hθ : ∀ (z : α), 1 ≤ θ z)
(hlim : Filter.Tendsto θ l Filter.atTop)
(u : Fin 2 → ↑unitInterval)
:
Filter.Tendsto (fun (z : α) => (genestGhoudi (θ z) ⋯).cdf u) l (nhds ((comonotonic 2).cdf u))
Genest–Ghoudi converges pointwise to the upper Fréchet bound on the closed square.