← Mathematical handbook

Nelsen 2 infinite-parameter endpoint

The truncated-power family converges pointwise on the closed square to the comonotonic copula for any real parameter path tending to infinity.

theorem ProbabilityTheory.Copula.twoTermPowerNorm_le (p a b : ℝ) (hp : 0 < p) (ha : 0 ≤ a) (hb : 0 ≤ b) : (a ^ p + b ^ p) ^ p⁻¹ ≤ 2 ^ p⁻¹ * max a b

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

Nelsen 2 converges pointwise to the upper Fréchet bound as θ tends to infinity.