← Copula mathematical handbook

Nelsen's family 18

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

The generator is non-strict (φ(0) = e^(-θ), and φ(1) = 0 as the limit t → 1⁻, imposed explicitly here). The pseudo-inverse is ψ(s) = 1 + θ / ln (min s e^(-θ)), built with BivariateGenerator.ofClamp. On (0, e^(-θ)) one has ln s < -θ ≤ -2 and ψ''(s) = θ ln s (ln s + 2) / (s ln² s)² ≥ 0; this is exactly where θ ≥ 2 is needed. At s = 0 Lean's convention ln 0 = 0 gives ψ(0) = 1, which is also the limit.

noncomputable def ProbabilityTheory.Copula.nelsen18Phi (θ : ℝ) (u : ↑unitInterval) : ℝ

The generator u ↦ exp (θ / (u - 1)) of family 18, with its value 0 at u = 1.

Equations

• ProbabilityTheory.Copula.nelsen18Phi θ u = if u = 1 then 0 else Real.exp (θ / (↑u - 1))

noncomputable def ProbabilityTheory.Copula.nelsen18Generator (θ : ℝ) (hθ : 2 ≤ θ) : BivariateGenerator

The clamped pseudo-inverse s ↦ 1 + θ / ln (min s e^(-θ)) of Nelsen's family 18, for θ ≥ 2. Its generator is u ↦ exp (θ / (u - 1)) (with value 0 at u = 1).

Equations

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

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

Nelsen's family 18 for θ ≥ 2.

Equations

• ProbabilityTheory.Copula.nelsen18 θ hθ = (ProbabilityTheory.Copula.nelsen18Generator θ hθ).copula

theorem ProbabilityTheory.Copula.isArchimedean_nelsen18 (θ : ℝ) (hθ : 2 ≤ θ) : (nelsen18 θ hθ).IsArchimedean

theorem ProbabilityTheory.Copula.nelsen18Generator_toFun_of_le (θ : ℝ) (hθ : 2 ≤ θ) {s : ℝ} (hs : Real.exp (-θ) ≤ s) : (nelsen18Generator θ hθ).toFun s = 0

The generator of family 18 is non-strict: its pseudo-inverse vanishes from e^(-θ) on.

theorem ProbabilityTheory.Copula.cdf_nelsen18 (θ : ℝ) (hθ : 2 ≤ θ) (u v : ↑unitInterval) (hu : u ≠ 0) (hu1 : u ≠ 1) (hv : v ≠ 0) (hv1 : v ≠ 1) : (nelsen18 θ hθ).cdf ![u, v] = max (1 + θ / Real.log (Real.exp (θ / (↑u - 1)) + Real.exp (θ / (↑v - 1)))) 0

The CDF of Nelsen's family 18 on the open unit square: C(u, v) = max (1 + θ / ln (exp (θ / (u - 1)) + exp (θ / (v - 1)))) 0.