← Copula mathematical handbook

Nelsen's family 19

Nelsen, An Introduction to Copulas, second edition, Table 4.1, number 19 (Section 4.2): generator φ(t) = exp (θ / t) - exp θ, inverse generator ψ(s) = θ / log (s + exp θ), and copula C(u, v) = θ / log (exp (θ / u) + exp (θ / v) - exp θ), for θ > 0.

The inverse generator is a positive constant divided by a positive concave function, hence convex. This is the full parameter range of Nelsen's table (the limiting case θ = 0 is not a member of the family in this module).

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

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

Equations

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

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

Nelsen's family 19 for θ > 0.

Equations

• ProbabilityTheory.Copula.nelsen19 θ hθ = (ProbabilityTheory.Copula.nelsen19Generator θ hθ).copula

theorem ProbabilityTheory.Copula.isArchimedean_nelsen19 (θ : ℝ) (hθ : 0 < θ) : (nelsen19 θ hθ).IsArchimedean

theorem ProbabilityTheory.Copula.cdf_nelsen19 (θ : ℝ) (hθ : 0 < θ) (u : Fin 2 → ↑unitInterval) (hu : ∀ (i : Fin 2), u i ≠ 0) : (nelsen19 θ hθ).cdf u = θ / Real.log (Real.exp (θ / ↑(u 0)) + Real.exp (θ / ↑(u 1)) - Real.exp θ)

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

theorem ProbabilityTheory.Copula.nelsen19_cdf_full (θ : ℝ) (hθ : 0 < θ) (u v : ↑unitInterval) : (nelsen19 θ hθ).cdf ![u, v] = if u = 0 ∨ v = 0 then 0 else θ / Real.log (Real.exp (θ / ↑u) + Real.exp (θ / ↑v) - Real.exp θ)

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