← Copula mathematical handbook

Limits at θ → 0⁺ of Nelsen's families 11 and 22

Nelsen, An Introduction to Copulas, second edition, Table 4.1 lists the limiting case C₀ = Π for family 11 (C(u, v) = max(u^θ v^θ − 2(1 − u^θ)(1 − v^θ), 0)^{1/θ}) and for family 22 (C(u, v) = (1 − a √(1 − b²) − b √(1 − a²))^{1/θ} with a = 1 − u^θ, b = 1 − v^θ, on the region a² + b² ≤ 1). Both are proved as pointwise convergence of the CDFs along any filter on which the parameter tends to 0 through admissible values (tendsto_nelsen11_zero, tendsto_nelsen22_zero).

Both follow from one elementary limit (tendsto_max_rpow_inv_nhdsGT_zero): if F(0) = 1 and F'(0) = c, then max(F(θ), 0)^{1/θ} → e^c as θ → 0⁺, since log F(θ) / θ → c. For both families F'(0) = log u + log v, so the limit is e^{log u + log v} = uv.

theorem ProbabilityTheory.Copula.tendsto_max_rpow_inv_nhdsGT_zero {F : ℝ → ℝ} {c : ℝ} (hF0 : F 0 = 1) (hF : HasDerivAt F c 0) : Filter.Tendsto (fun (t : ℝ) => max (F t) 0 ^ t⁻¹) (nhdsWithin 0 (Set.Ioi 0)) (nhds (Real.exp c))

If F(0) = 1 and F'(0) = c, then max(F(θ), 0)^{1/θ} → e^c as θ → 0⁺.

theorem ProbabilityTheory.Copula.tendsto_nelsen11_zero {α : Type u_1} {l : Filter α} (θ : α → ℝ) (hθ : ∀ (a : α), 0 < θ a) (h2 : ∀ (a : α), θ a ≤ 1 / 2) (hlim : Filter.Tendsto θ l (nhds 0)) (u : Fin 2 → ↑unitInterval) : Filter.Tendsto (fun (a : α) => (nelsen11 (θ a) ⋯ ⋯).cdf u) l (nhds ((independence 2).cdf u))

The limit Π of Nelsen's family 11 as θ → 0⁺ (Table 4.1), pointwise on the unit square.

theorem ProbabilityTheory.Copula.tendsto_nelsen22_zero {α : Type u_1} {l : Filter α} (θ : α → ℝ) (hθ : ∀ (a : α), 0 < θ a) (h1 : ∀ (a : α), θ a ≤ 1) (hlim : Filter.Tendsto θ l (nhds 0)) (u : Fin 2 → ↑unitInterval) : Filter.Tendsto (fun (a : α) => (nelsen22 (θ a) ⋯ ⋯).cdf u) l (nhds ((independence 2).cdf u))

The limit Π of Nelsen's family 22 as θ → 0⁺ (Table 4.1), pointwise on the unit square.