← Copula mathematical handbook

Nelsen's family 11

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

The generator is non-strict (φ(0) = ln 2), so the inverse generator is the clamped function ψ(s) = (2 - exp (min s (ln 2)))^(1/θ) built with BivariateGenerator.ofClamp. With p = 1/θ ≥ 2, convexity on [0, ln 2] follows from ψ''(s) = p eˢ (2 - eˢ)^(p - 2) (p eˢ - 2) ≥ 0; this is exactly where θ ≤ 1/2 is needed.

noncomputable def ProbabilityTheory.Copula.nelsen11Generator (θ : ℝ) (hθ : 0 < θ) (h2 : θ ≤ 1 / 2) : BivariateGenerator

The clamped inverse generator s ↦ (2 - exp (min s (ln 2)))^(1/θ) of Nelsen's family 11, for 0 < θ ≤ 1/2. Its generator is u ↦ ln (2 - u^θ).

Equations

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

noncomputable def ProbabilityTheory.Copula.nelsen11 (θ : ℝ) (hθ : 0 < θ) (h2 : θ ≤ 1 / 2) : Copula 2

Nelsen's family 11 for 0 < θ ≤ 1/2.

Equations

• ProbabilityTheory.Copula.nelsen11 θ hθ h2 = (ProbabilityTheory.Copula.nelsen11Generator θ hθ h2).copula

theorem ProbabilityTheory.Copula.isArchimedean_nelsen11 (θ : ℝ) (hθ : 0 < θ) (h2 : θ ≤ 1 / 2) : (nelsen11 θ hθ h2).IsArchimedean

theorem ProbabilityTheory.Copula.nelsen11Generator_invFun (θ : ℝ) (hθ : 0 < θ) (h2 : θ ≤ 1 / 2) (u : ↑unitInterval) : (nelsen11Generator θ hθ h2).invFun u = Real.log (2 - ↑u ^ θ)

The generator of Nelsen's family 11 is u ↦ ln (2 - u^θ).

theorem ProbabilityTheory.Copula.nelsen11Generator_toFun_of_le (θ : ℝ) (hθ : 0 < θ) (h2 : θ ≤ 1 / 2) {s : ℝ} (hs : Real.log 2 ≤ s) : (nelsen11Generator θ hθ h2).toFun s = 0

The generator of family 11 is non-strict: its pseudo-inverse vanishes from ln 2 on.

theorem ProbabilityTheory.Copula.cdf_nelsen11 (θ : ℝ) (hθ : 0 < θ) (h2 : θ ≤ 1 / 2) (u v : ↑unitInterval) (hu : u ≠ 0) (hv : v ≠ 0) : (nelsen11 θ hθ h2).cdf ![u, v] = max (↑u ^ θ * ↑v ^ θ - 2 * (1 - ↑u ^ θ) * (1 - ↑v ^ θ)) 0 ^ θ⁻¹

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

theorem ProbabilityTheory.Copula.nelsen11_cdf_full (θ : ℝ) (hθ : 0 < θ) (h2 : θ ≤ 1 / 2) (u v : ↑unitInterval) : (nelsen11 θ hθ h2).cdf ![u, v] = if u = 0 ∨ v = 0 then 0 else max (↑u ^ θ * ↑v ^ θ - 2 * (1 - ↑u ^ θ) * (1 - ↑v ^ θ)) 0 ^ θ⁻¹

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