← Copula mathematical handbook

Nelsen's family 17

Nelsen, An Introduction to Copulas, second edition, Table 4.1, number 17 (Section 4.2): generator φ(t) = -ln (((1 + t)^(-θ) - 1) / (2^(-θ) - 1)) for θ ≠ 0 and copula C(u, v) = (1 + ((1 + u)^(-θ) - 1) ((1 + v)^(-θ) - 1) / (2^(-θ) - 1))^(-1/θ) - 1.

With d = 2^(-θ) - 1 > -1 and q = -1/θ, the inverse generator is ψ(s) = (1 + d e^(-s))^q - 1. Its second derivative is ψ''(s) = q d e^(-s) (1 + d e^(-s))^(q - 2) (1 + q d e^(-s)), which is nonnegative because q d = (1 - 2^(-θ)) / θ > 0 for every θ ≠ 0. This covers Nelsen's whole parameter range, both signs of θ at once. At θ = -1 the family is independence (C_{-1} = Π).

noncomputable def ProbabilityTheory.Copula.nelsen17Generator (θ : ℝ) (hθ : θ ≠ 0) : BivariateGenerator

The inverse generator s ↦ (1 + (2^(-θ) - 1) e^(-s))^(-1/θ) - 1 of Nelsen's family 17, for θ ≠ 0. Its generator is u ↦ -ln (((1 + u)^(-θ) - 1) / (2^(-θ) - 1)).

Equations

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

noncomputable def ProbabilityTheory.Copula.nelsen17 (θ : ℝ) (hθ : θ ≠ 0) : Copula 2

Nelsen's family 17 for θ ≠ 0.

Equations

• ProbabilityTheory.Copula.nelsen17 θ hθ = (ProbabilityTheory.Copula.nelsen17Generator θ hθ).copula

theorem ProbabilityTheory.Copula.isArchimedean_nelsen17 (θ : ℝ) (hθ : θ ≠ 0) : (nelsen17 θ hθ).IsArchimedean

theorem ProbabilityTheory.Copula.cdf_nelsen17 (θ : ℝ) (hθ : θ ≠ 0) (u v : ↑unitInterval) (hu : u ≠ 0) (hv : v ≠ 0) : (nelsen17 θ hθ).cdf ![u, v] = (1 + ((1 + ↑u) ^ (-θ) - 1) * ((1 + ↑v) ^ (-θ) - 1) / (2 ^ (-θ) - 1)) ^ (-θ⁻¹) - 1

The CDF of Nelsen's family 17 on positive coordinates: C(u, v) = (1 + ((1 + u)^(-θ) - 1) ((1 + v)^(-θ) - 1) / (2^(-θ) - 1))^(-1/θ) - 1.

theorem ProbabilityTheory.Copula.nelsen17_cdf_full (θ : ℝ) (hθ : θ ≠ 0) (u v : ↑unitInterval) : (nelsen17 θ hθ).cdf ![u, v] = if u = 0 ∨ v = 0 then 0 else (1 + ((1 + ↑u) ^ (-θ) - 1) * ((1 + ↑v) ^ (-θ) - 1) / (2 ^ (-θ) - 1)) ^ (-θ⁻¹) - 1

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

theorem ProbabilityTheory.Copula.nelsen17Generator_neg_one : nelsen17Generator (-1) ⋯ = exponentialGenerator

At θ = -1 the generator of family 17 is the exponential generator of independence.

@[simp]

theorem ProbabilityTheory.Copula.nelsen17_neg_one : nelsen17 (-1) ⋯ = independence 2

C_{-1} = Π: at θ = -1 Nelsen's family 17 is independence.