← Copula mathematical handbook

Nelsen's family 10

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

No new convexity argument is needed: the inverse generator is ψ(s) = (2 / (exp s + 1))^(1/θ), the 1/θ-th power of the inverse generator of the Ali--Mikhail--Haq family at parameter -1, so the family is innerPower of amhGenerator (-1) with exponent 1/θ ≥ 1. This is the full parameter range of Nelsen's table (the limiting case θ = 0, independence, is not a member of the family in this module).

noncomputable def ProbabilityTheory.Copula.nelsen10Generator (θ : ℝ) (hθ : 0 < θ) (h1 : θ ≤ 1) : BivariateGenerator

The inverse generator s ↦ (2 / (exp s + 1))^(1/θ) of Nelsen's family 10, for 0 < θ ≤ 1: the 1/θ-th inner power of the Ali--Mikhail--Haq generator at -1.

Equations

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

noncomputable def ProbabilityTheory.Copula.nelsen10 (θ : ℝ) (hθ : 0 < θ) (h1 : θ ≤ 1) : Copula 2

Nelsen's family 10 for 0 < θ ≤ 1.

Equations

• ProbabilityTheory.Copula.nelsen10 θ hθ h1 = (ProbabilityTheory.Copula.nelsen10Generator θ hθ h1).copula

theorem ProbabilityTheory.Copula.isArchimedean_nelsen10 (θ : ℝ) (hθ : 0 < θ) (h1 : θ ≤ 1) : (nelsen10 θ hθ h1).IsArchimedean

theorem ProbabilityTheory.Copula.nelsen10Generator_invFun (θ : ℝ) (hθ : 0 < θ) (h1 : θ ≤ 1) (u : ↑unitInterval) : (nelsen10Generator θ hθ h1).invFun u = Real.log (2 * ↑u ^ (-θ) - 1)

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

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

Nelsen's family 10: C(u,v) = u v / (1 + (1 - u^θ)(1 - v^θ))^(1/θ) on positive coordinates.

theorem ProbabilityTheory.Copula.nelsen10_cdf_full (θ : ℝ) (hθ : 0 < θ) (h1 : θ ≤ 1) (u v : ↑unitInterval) : (nelsen10 θ hθ h1).cdf ![u, v] = if u = 0 ∨ v = 0 then 0 else ↑u * ↑v / (1 + (1 - ↑u ^ θ) * (1 - ↑v ^ θ)) ^ θ⁻¹

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