← Copula mathematical handbook

Nelsen 12 infinite-parameter endpoint

The positive-coordinate CDF is a reciprocal of a two-coordinate power norm. Its pointwise limit is comonotonicity, including the grounded axes.

theorem ProbabilityTheory.Copula.tendsto_twoTermPowerNorm {α : Type u_1} {l : Filter α} (θ : α → ℝ) (hθ : ∀ (z : α), 1 ≤ θ z) (hlim : Filter.Tendsto θ l Filter.atTop) (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) : Filter.Tendsto (fun (z : α) => (a ^ θ z + b ^ θ z) ^ (θ z)⁻¹) l (nhds (max a b))

theorem ProbabilityTheory.Copula.tendsto_nelsen12_atTop {α : Type u_1} {l : Filter α} (θ : α → ℝ) (hθ : ∀ (z : α), 1 ≤ θ z) (hlim : Filter.Tendsto θ l Filter.atTop) (u : Fin 2 → ↑unitInterval) : Filter.Tendsto (fun (z : α) => (nelsen12 (θ z) ⋯).cdf u) l (nhds ((comonotonic 2).cdf u))

Nelsen 12 converges pointwise to the upper Fréchet bound.