← Copula mathematical handbook

Nelsen's family 20

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

The inverse generator is a positive concave function raised to a nonpositive power, 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.nelsen20Generator (θ : ℝ) (hθ : 0 < θ) : BivariateGenerator

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

Equations

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

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

Nelsen's family 20 for θ > 0.

Equations

• ProbabilityTheory.Copula.nelsen20 θ hθ = (ProbabilityTheory.Copula.nelsen20Generator θ hθ).copula

theorem ProbabilityTheory.Copula.isArchimedean_nelsen20 (θ : ℝ) (hθ : 0 < θ) : (nelsen20 θ hθ).IsArchimedean

theorem ProbabilityTheory.Copula.cdf_nelsen20 (θ : ℝ) (hθ : 0 < θ) (u : Fin 2 → ↑unitInterval) (hu : ∀ (i : Fin 2), u i ≠ 0) : (nelsen20 θ hθ).cdf u = Real.log (Real.exp (↑(u 0) ^ (-θ)) + Real.exp (↑(u 1) ^ (-θ)) - Real.exp 1) ^ (-θ⁻¹)

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

theorem ProbabilityTheory.Copula.nelsen20_cdf_full (θ : ℝ) (hθ : 0 < θ) (u v : ↑unitInterval) : (nelsen20 θ hθ).cdf ![u, v] = if u = 0 ∨ v = 0 then 0 else Real.log (Real.exp (↑u ^ (-θ)) + Real.exp (↑v ^ (-θ)) - Real.exp 1) ^ (-θ⁻¹)

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