← Copula mathematical handbook

Nelsen's family 13

Nelsen, An Introduction to Copulas, second edition, Table 4.1, number 13 (Section 4.2): generator φ(t) = (1 - ln t)^θ - 1, inverse generator ψ(s) = exp (1 - (1 + s)^(1/θ)), and copula C(u, v) = exp (1 - ((1 - ln u)^θ + (1 - ln v)^θ - 1)^(1/θ)).

This module covers Nelsen's whole parameter range θ > 0. Convexity of the inverse generator is proved from its second derivative: with p = 1/θ, ψ''(s) = p ψ(s) (1 + s)^(p - 2) (p (1 + s)^p - (p - 1)) ≥ 0, since (1 + s)^p ≥ 1. At θ = 1 the family is independence (C_1 = Π in Nelsen's table).

noncomputable def ProbabilityTheory.Copula.nelsen13Generator (θ : ℝ) (hθ : 0 < θ) : BivariateGenerator

The inverse generator s ↦ exp (1 - (1 + s)^(1/θ)) of Nelsen's family 13, for θ > 0. Its generator is u ↦ (1 - ln u)^θ - 1.

Equations

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

noncomputable def ProbabilityTheory.Copula.nelsen13 (θ : ℝ) (hθ : 0 < θ) : Copula 2

Nelsen's family 13 for θ > 0.

Equations

• ProbabilityTheory.Copula.nelsen13 θ hθ = (ProbabilityTheory.Copula.nelsen13Generator θ hθ).copula

theorem ProbabilityTheory.Copula.isArchimedean_nelsen13 (θ : ℝ) (hθ : 0 < θ) : (nelsen13 θ hθ).IsArchimedean

theorem ProbabilityTheory.Copula.cdf_nelsen13 (θ : ℝ) (hθ : 0 < θ) (u : Fin 2 → ↑unitInterval) (hu : ∀ (i : Fin 2), u i ≠ 0) : (nelsen13 θ hθ).cdf u = Real.exp (1 - ((1 - Real.log ↑(u 0)) ^ θ + (1 - Real.log ↑(u 1)) ^ θ - 1) ^ θ⁻¹)

The CDF of Nelsen's family 13 on positive coordinates.

theorem ProbabilityTheory.Copula.nelsen13_cdf_full (θ : ℝ) (hθ : 0 < θ) (u v : ↑unitInterval) : (nelsen13 θ hθ).cdf ![u, v] = if u = 0 ∨ v = 0 then 0 else Real.exp (1 - ((1 - Real.log ↑u) ^ θ + (1 - Real.log ↑v) ^ θ - 1) ^ θ⁻¹)

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

@[simp]

theorem ProbabilityTheory.Copula.nelsen13_one : nelsen13 1 ⋯ = independence 2

At θ = 1 Nelsen's family 13 is independence.