Gumbel–Hougaard infinite-parameter endpoint #
The positive-coordinate CDF is the exponential of a two-coordinate power norm. Its pointwise limit is comonotonicity, with grounded axes handled separately.
theorem
ProbabilityTheory.Copula.tendsto_gumbel_atTop
{α : Type u_1}
{l : Filter α}
(θ : α → ℝ)
(hθ : ∀ (z : α), 1 ≤ θ z)
(hlim : Filter.Tendsto θ l Filter.atTop)
(u : Fin 2 → ↑unitInterval)
:
Filter.Tendsto (fun (z : α) => (gumbel (θ z) ⋯).cdf u) l (nhds ((comonotonic 2).cdf u))
Gumbel–Hougaard converges pointwise to the upper Fréchet bound.