← Copula mathematical handbook

Nelsen's family 21

Nelsen, An Introduction to Copulas, second edition, Table 4.1, number 21 (Section 4.2): generator φ(t) = 1 - (1 - (1 - t)^θ)^(1/θ) for θ ≥ 1 and copula C(u, v) = 1 - (1 - (max (A + B - 1) 0)^θ)^(1/θ) with A = (1 - (1 - u)^θ)^(1/θ) and B = (1 - (1 - v)^θ)^(1/θ).

The generator is non-strict (φ(0) = 1) and is an involution of [0, 1], so the pseudo-inverse is ψ(s) = φ(min s 1), built with BivariateGenerator.ofClamp. Convexity needs no derivatives: φ = G ∘ h with h(s) = 1 - (1 - s)^θ concave and G(z) = 1 - z^(1/θ) convex and antitone on [0, 1]. (Geometrically, z ↦ (1 - z^θ)^(1/θ) is the boundary of the unit ℓ^θ ball.) At θ = 1 the family is the lower Fréchet bound (C_1 = W).

noncomputable def ProbabilityTheory.Copula.nelsen21Fun (θ t : ℝ) : ℝ

The generator (and, on [0, 1], its own inverse) t ↦ 1 - (1 - (1 - t)^θ)^(1/θ) of Nelsen's family 21.

Equations

• ProbabilityTheory.Copula.nelsen21Fun θ t = 1 - (1 - (1 - t) ^ θ) ^ θ⁻¹

theorem ProbabilityTheory.Copula.nelsen21Fun_mem (θ : ℝ) (hθ : 1 ≤ θ) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : nelsen21Fun θ t ∈ Set.Icc 0 1

theorem ProbabilityTheory.Copula.nelsen21Fun_nelsen21Fun (θ : ℝ) (hθ : 1 ≤ θ) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : nelsen21Fun θ (nelsen21Fun θ t) = t

The generator of family 21 is an involution of [0, 1].

theorem ProbabilityTheory.Copula.nelsen21Fun_convexOn (θ : ℝ) (hθ : 1 ≤ θ) : ConvexOn ℝ (Set.Icc 0 1) (nelsen21Fun θ)

theorem ProbabilityTheory.Copula.nelsen21Fun_antitoneOn (θ : ℝ) (hθ : 1 ≤ θ) : AntitoneOn (nelsen21Fun θ) (Set.Icc 0 1)

theorem ProbabilityTheory.Copula.nelsen21Fun_one (θ : ℝ) (hθ : 1 ≤ θ) : nelsen21Fun θ 1 = 0

noncomputable def ProbabilityTheory.Copula.nelsen21Generator (θ : ℝ) (hθ : 1 ≤ θ) : BivariateGenerator

The clamped pseudo-inverse s ↦ φ(min s 1) of Nelsen's family 21, for θ ≥ 1. The generator is φ(u) = 1 - (1 - (1 - u)^θ)^(1/θ).

Equations

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

noncomputable def ProbabilityTheory.Copula.nelsen21 (θ : ℝ) (hθ : 1 ≤ θ) : Copula 2

Nelsen's family 21 for θ ≥ 1.

Equations

• ProbabilityTheory.Copula.nelsen21 θ hθ = (ProbabilityTheory.Copula.nelsen21Generator θ hθ).copula

theorem ProbabilityTheory.Copula.isArchimedean_nelsen21 (θ : ℝ) (hθ : 1 ≤ θ) : (nelsen21 θ hθ).IsArchimedean

theorem ProbabilityTheory.Copula.cdf_nelsen21 (θ : ℝ) (hθ : 1 ≤ θ) (u v : ↑unitInterval) (hu : u ≠ 0) (hv : v ≠ 0) : (nelsen21 θ hθ).cdf ![u, v] = 1 - (1 - max ((1 - (1 - ↑u) ^ θ) ^ θ⁻¹ + (1 - (1 - ↑v) ^ θ) ^ θ⁻¹ - 1) 0 ^ θ) ^ θ⁻¹

The CDF of Nelsen's family 21 on positive coordinates: C(u, v) = 1 - (1 - (max (A + B - 1) 0)^θ)^(1/θ) with A = (1 - (1 - u)^θ)^(1/θ), B = (1 - (1 - v)^θ)^(1/θ).

theorem ProbabilityTheory.Copula.nelsen21_cdf_full (θ : ℝ) (hθ : 1 ≤ θ) (u v : ↑unitInterval) : (nelsen21 θ hθ).cdf ![u, v] = if u = 0 ∨ v = 0 then 0 else 1 - (1 - max ((1 - (1 - ↑u) ^ θ) ^ θ⁻¹ + (1 - (1 - ↑v) ^ θ) ^ θ⁻¹ - 1) 0 ^ θ) ^ θ⁻¹

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

theorem ProbabilityTheory.Copula.nelsen21Generator_one : nelsen21Generator 1 ⋯ = truncatedLinearGenerator

At θ = 1 the generator of family 21 is the truncated linear generator of W.

@[simp]

theorem ProbabilityTheory.Copula.nelsen21_one : nelsen21 1 ⋯ = countermonotonic

C_1 = W: at θ = 1 Nelsen's family 21 is the lower Fréchet bound.