← Copula mathematical handbook

Nelsen's family 16

Nelsen, An Introduction to Copulas, second edition, Table 4.1, number 16 (Section 4.2): generator φ(t) = (θ / t + 1) (1 - t) for θ ≥ 0 and copula C(u, v) = (S + √(S² + 4θ)) / 2 with S = u + v - 1 - θ (1/u + 1/v - 1).

Solving the quadratic t² + (s - 1 + θ) t - θ = 0 gives the inverse generator ψ(s) = (1 - θ - s + √((1 - θ - s)² + 4θ)) / 2. It is convex because x ↦ √(x² + c) is convex (a Euclidean norm), and antitone because x ↦ x + √(x² + c) is monotone. No derivatives are needed. The generator is strict for θ > 0; at θ = 0 the same formulas give ψ(s) = max 0 (1 - s) and the family is the lower Fréchet bound W, as in Nelsen's table (C_0 = W).

theorem ProbabilityTheory.Copula.sqrt_sq_add_convex_ineq {c : ℝ} (hc : 0 ≤ c) (x y a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) : √((a * x + b * y) ^ 2 + c) ≤ a * √(x ^ 2 + c) + b * √(y ^ 2 + c)

x ↦ √(x² + c) is convex for c ≥ 0 (the inequality form).

theorem ProbabilityTheory.Copula.add_sqrt_sq_add_mono {c : ℝ} (hc : 0 ≤ c) {x y : ℝ} (hxy : x ≤ y) : x + √(x ^ 2 + c) ≤ y + √(y ^ 2 + c)

x ↦ x + √(x² + c) is monotone.

theorem ProbabilityTheory.Copula.add_sqrt_sq_add_nonneg {c : ℝ} (hc : 0 ≤ c) (x : ℝ) : 0 ≤ x + √(x ^ 2 + c)

x + √(x² + c) ≥ 0.

noncomputable def ProbabilityTheory.Copula.nelsen16Generator (θ : ℝ) (hθ : 0 ≤ θ) : BivariateGenerator

The inverse generator s ↦ (1 - θ - s + √((1 - θ - s)² + 4θ)) / 2 of Nelsen's family 16, for θ ≥ 0. Its generator is u ↦ (θ / u + 1) (1 - u).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ProbabilityTheory.Copula.nelsen16 (θ : ℝ) (hθ : 0 ≤ θ) : Copula 2

Nelsen's family 16 for θ ≥ 0.

Equations

• ProbabilityTheory.Copula.nelsen16 θ hθ = (ProbabilityTheory.Copula.nelsen16Generator θ hθ).copula

theorem ProbabilityTheory.Copula.isArchimedean_nelsen16 (θ : ℝ) (hθ : 0 ≤ θ) : (nelsen16 θ hθ).IsArchimedean

theorem ProbabilityTheory.Copula.cdf_nelsen16 (θ : ℝ) (hθ : 0 ≤ θ) (u v : ↑unitInterval) (hu : u ≠ 0) (hv : v ≠ 0) : (nelsen16 θ hθ).cdf ![u, v] = (↑u + ↑v - 1 - θ * (1 / ↑u + 1 / ↑v - 1) + √((↑u + ↑v - 1 - θ * (1 / ↑u + 1 / ↑v - 1)) ^ 2 + 4 * θ)) / 2

The CDF of Nelsen's family 16 on positive coordinates: C(u, v) = (S + √(S² + 4θ)) / 2 with S = u + v - 1 - θ (1/u + 1/v - 1).

theorem ProbabilityTheory.Copula.nelsen16_cdf_full (θ : ℝ) (hθ : 0 ≤ θ) (u v : ↑unitInterval) : (nelsen16 θ hθ).cdf ![u, v] = if u = 0 ∨ v = 0 then 0 else (↑u + ↑v - 1 - θ * (1 / ↑u + 1 / ↑v - 1) + √((↑u + ↑v - 1 - θ * (1 / ↑u + 1 / ↑v - 1)) ^ 2 + 4 * θ)) / 2

Nelsen's family 16 on the whole closed unit square, with grounded zero axes.

theorem ProbabilityTheory.Copula.nelsen16Generator_zero : nelsen16Generator 0 ⋯ = truncatedLinearGenerator

At θ = 0 the generator of family 16 is the truncated linear generator of W.

@[simp]

theorem ProbabilityTheory.Copula.nelsen16_zero : nelsen16 0 ⋯ = countermonotonic

C_0 = W: at θ = 0 Nelsen's family 16 is the lower Fréchet bound.