← Copula mathematical handbook

Limits at θ → ∞ of Nelsen's families 17 and 21

Nelsen, An Introduction to Copulas, second edition, Table 4.1 lists the limiting case C_∞ = M for families 17 and 21. Both are proved here as pointwise convergence of the CDFs along any filter on which the parameter tends to +∞ (tendsto_nelsen21_atTop, tendsto_nelsen17_atTop). Since every copula lies below M, only a lower bound is needed:

• family 21: with s = 1 − u, t = 1 − v, w = max(s, t), Bernoulli's inequality gives C_θ(u, v) ≥ 1 − (2θ)^{1/θ} w, and (2θ)^{1/θ} → 1;
• family 17: with z = min(u, v), C_θ(u, v) ≥ (2 / (1 − 2^{−θ}))^{−1/θ} (1 + z) − 1, and the factor tends to 1.

For family 17 at θ → −∞ the limit is not W: it is max(0, ((1 + u)(1 + v) − 2)/2) = max(0, (uv + u + v − 1)/2), the member θ = 1/2 of family 7 (tendsto_nelsen17_atBot). With κ = −θ, r = (1 + u)(1 + v)/2 and P = (1 − (1 + u)^{−κ})(1 − (1 + v)^{−κ}), the CDF satisfies max(1, rP) − 1 ≤ C_θ(u, v) ≤ 3^{1/κ} max(1, r) − 1 (nelsen17_bounds_neg).

theorem ProbabilityTheory.Copula.tendsto_two_mul_rpow_inv_atTop : Filter.Tendsto (fun (r : ℝ) => (2 * r) ^ r⁻¹) Filter.atTop (nhds 1)

(2r)^{1/r} → 1 as r → ∞.

theorem ProbabilityTheory.Copula.nelsen21_lower_bound (θ : ℝ) (hθ : 1 ≤ θ) {x y : ℝ} (hx0 : 0 ≤ x) (hx1 : x ≤ 1) (hy0 : 0 ≤ y) (hy1 : y ≤ 1) : 1 - (2 * θ) ^ θ⁻¹ * max (1 - x) (1 - y) ≤ 1 - (1 - max ((1 - (1 - x) ^ θ) ^ θ⁻¹ + (1 - (1 - y) ^ θ) ^ θ⁻¹ - 1) 0 ^ θ) ^ θ⁻¹

The lower bound C_θ(u, v) ≥ 1 − (2θ)^{1/θ} max(1 − u, 1 − v) for family 21.

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

The limit M of Nelsen's family 21 as θ → ∞ (Table 4.1), pointwise on the unit square.

theorem ProbabilityTheory.Copula.nelsen17_lower_bound (θ : ℝ) (hθ : 0 < θ) {x y : ℝ} (hx0 : 0 < x) (hx1 : x ≤ 1) (hy0 : 0 < y) (hy1 : y ≤ 1) : (2 / (1 - 2 ^ (-θ))) ^ (-θ⁻¹) * (1 + min x y) - 1 ≤ (1 + ((1 + x) ^ (-θ) - 1) * ((1 + y) ^ (-θ) - 1) / (2 ^ (-θ) - 1)) ^ (-θ⁻¹) - 1

The lower bound C_θ(u, v) ≥ (2 / (1 − 2^{−θ}))^{−1/θ} (1 + min(u, v)) − 1 for family 17, θ > 0, u, v ∈ (0, 1].

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

The limit M of Nelsen's family 17 as θ → ∞ (Table 4.1), pointwise on the unit square.

theorem ProbabilityTheory.Copula.nelsen17_bounds_neg (θ : ℝ) (hθ : θ ≤ -1) {x y : ℝ} (hx0 : 0 < x) (hy0 : 0 < y) : max 1 ((1 + x) * (1 + y) / 2 * ((1 - ((1 + x) ^ (-θ))⁻¹) * (1 - ((1 + y) ^ (-θ))⁻¹))) - 1 ≤ (1 + ((1 + x) ^ (-θ) - 1) * ((1 + y) ^ (-θ) - 1) / (2 ^ (-θ) - 1)) ^ (-θ⁻¹) - 1 ∧ (1 + ((1 + x) ^ (-θ) - 1) * ((1 + y) ^ (-θ) - 1) / (2 ^ (-θ) - 1)) ^ (-θ⁻¹) - 1 ≤ 3 ^ (-θ)⁻¹ * max 1 ((1 + x) * (1 + y) / 2) - 1

Two-sided bounds for family 17 at negative parameters θ ≤ −1 (with κ = −θ): max(1, r P) − 1 ≤ C_θ(u, v) ≤ 3^{1/κ} max(1, r) − 1, r = (1 + u)(1 + v)/2, P = (1 − (1 + u)^{−κ})(1 − (1 + v)^{−κ}).

theorem ProbabilityTheory.Copula.tendsto_nelsen17_atBot {α : Type u_1} {l : Filter α} (θ : α → ℝ) (hθ : ∀ (a : α), θ a < 0) (hlim : Filter.Tendsto θ l Filter.atBot) (u : Fin 2 → ↑unitInterval) : Filter.Tendsto (fun (a : α) => (nelsen17 (θ a) ⋯).cdf u) l (nhds ((nelsen7 ⟨1 / 2, ⋯⟩).cdf u))

The limit of Nelsen's family 17 as θ → −∞: pointwise convergence to max(0, (uv + u + v − 1)/2), the member θ = 1/2 of Nelsen's family 7 (not W).