← Copula mathematical handbook

Nelsen's family 9 (Gumbel–Barnett)

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

Convexity of ψ on [0, ∞) is proved from its second derivative ψ''(s) = (1/θ) ψ(s) exp s ((exp s)/θ - 1) ≥ 0, which is nonnegative exactly because θ ≤ 1 ≤ exp s. 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.nelsen9Generator (θ : ℝ) (hθ : 0 < θ) (h1 : θ ≤ 1) : BivariateGenerator

The inverse generator s ↦ exp ((1 - exp s) / θ) of the Gumbel–Barnett family, for 0 < θ ≤ 1. Its generator is u ↦ ln (1 - θ ln u).

Equations

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

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

Nelsen's family 9 (Gumbel–Barnett) for 0 < θ ≤ 1.

Equations

• ProbabilityTheory.Copula.nelsen9 θ hθ h1 = (ProbabilityTheory.Copula.nelsen9Generator θ hθ h1).copula

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

theorem ProbabilityTheory.Copula.cdf_nelsen9 (θ : ℝ) (hθ : 0 < θ) (h1 : θ ≤ 1) (u : Fin 2 → ↑unitInterval) (hu : ∀ (i : Fin 2), u i ≠ 0) : (nelsen9 θ hθ h1).cdf u = ↑(u 0) * ↑(u 1) * Real.exp (-(θ * Real.log ↑(u 0) * Real.log ↑(u 1)))

The Gumbel–Barnett CDF u v exp (-θ ln u ln v) on positive coordinates.

theorem ProbabilityTheory.Copula.nelsen9_cdf_full (θ : ℝ) (hθ : 0 < θ) (h1 : θ ≤ 1) (u v : ↑unitInterval) : (nelsen9 θ hθ h1).cdf ![u, v] = if u = 0 ∨ v = 0 then 0 else ↑u * ↑v * Real.exp (-(θ * Real.log ↑u * Real.log ↑v))

The Gumbel–Barnett CDF on the whole closed unit square, with grounded zero axes.