← Copula mathematical handbook

Construction of bivariate copulas with a prescribed diagonal

Given a function δ : I → ℝ satisfying the necessary conditions for a diagonal section (δ 1 = 1, 0 ≤ δ t ≤ t, δ increasing, and δ t' - δ t ≤ 2 (t' - t) for t ≤ t', see Copula.Diagonal), the function K u v = min (min u v) ((δ u + δ v) / 2) is the CDF of a bivariate copula with diagonal δ (Nelsen, An Introduction to Copulas, 2nd ed., §3.2.6: the construction of Fredricks and Nelsen, the diagonal copula of Bertino). This shows that the necessary conditions are also sufficient.

The rectangle inequality is proved by writing K u v = (δ u + δ v) / 2 - ((α v - β u)⁺ + (α u - β v)⁺) with α = δ / 2 and β t = t - δ t / 2 both increasing. The two positive parts cannot be positive simultaneously, and (α v - β u)⁺ has nonpositive mixed increments by convexity of x ↦ x⁺.

structure ProbabilityTheory.Copula.IsDiagonalFunction (δ : ↑unitInterval → ℝ) : Prop

The necessary conditions for a function to be the diagonal section of a bivariate copula.

• one : δ 1 = 1

  The diagonal takes the value one at one.

• nonneg (t : ↑unitInterval) : 0 ≤ δ t

  The diagonal is nonnegative.

• le_self (t : ↑unitInterval) : δ t ≤ ↑t

  The diagonal lies below the identity.

• monotone : Monotone δ

  The diagonal is increasing.

• lipschitz (s t : ↑unitInterval) : s ≤ t → δ t - δ s ≤ 2 * (↑t - ↑s)

  The diagonal is 2-Lipschitz.

theorem ProbabilityTheory.Copula.isDiagonalFunction_diagonal (C : Copula 2) : IsDiagonalFunction C.diagonal

The diagonal section of every bivariate copula satisfies the necessary conditions.

noncomputable def ProbabilityTheory.Copula.diagKernel (δ : ↑unitInterval → ℝ) (u v : ↑unitInterval) : ℝ

The Fredricks–Nelsen kernel min (min u v) ((δ u + δ v) / 2).

Equations

• ProbabilityTheory.Copula.diagKernel δ u v = min (min ↑u ↑v) ((δ u + δ v) / 2)

noncomputable def ProbabilityTheory.Copula.diagAlpha (δ : ↑unitInterval → ℝ) (t : ↑unitInterval) : ℝ

The increasing function δ / 2 used in the rectangle inequality.

Equations

• ProbabilityTheory.Copula.diagAlpha δ t = δ t / 2

noncomputable def ProbabilityTheory.Copula.diagBeta (δ : ↑unitInterval → ℝ) (t : ↑unitInterval) : ℝ

The increasing function t - δ t / 2 used in the rectangle inequality.

Equations

• ProbabilityTheory.Copula.diagBeta δ t = ↑t - δ t / 2

theorem ProbabilityTheory.Copula.IsDiagonalFunction.isClassical {δ : ↑unitInterval → ℝ} (hδ : IsDiagonalFunction δ) : IsClassical fun (u : Fin 2 → ↑unitInterval) => diagKernel δ (u 0) (u 1)

The Fredricks–Nelsen kernel of a diagonal function satisfies the classical copula conditions.

noncomputable def ProbabilityTheory.Copula.diagonalCopula (δ : ↑unitInterval → ℝ) (hδ : IsDiagonalFunction δ) : Copula 2

The bivariate copula with CDF min (min u v) ((δ u + δ v) / 2) (Fredricks–Nelsen).

Equations

• ProbabilityTheory.Copula.diagonalCopula δ hδ = ProbabilityTheory.Copula.ofClassical (fun (u : Fin 2 → ↑unitInterval) => ProbabilityTheory.Copula.diagKernel δ (u 0) (u 1)) ⋯

theorem ProbabilityTheory.Copula.cdf_diagonalCopula (δ : ↑unitInterval → ℝ) (hδ : IsDiagonalFunction δ) (u : Fin 2 → ↑unitInterval) : (diagonalCopula δ hδ).cdf u = diagKernel δ (u 0) (u 1)

The CDF of diagonalCopula δ is the Fredricks–Nelsen kernel.

theorem ProbabilityTheory.Copula.diagonal_diagonalCopula (δ : ↑unitInterval → ℝ) (hδ : IsDiagonalFunction δ) (t : ↑unitInterval) : (diagonalCopula δ hδ).diagonal t = δ t

The diagonal section of diagonalCopula δ is δ.

theorem ProbabilityTheory.Copula.isDiagonalFunction_iff_exists_copula (δ : ↑unitInterval → ℝ) : IsDiagonalFunction δ ↔ ∃ (C : Copula 2), C.diagonal = δ

A function is the diagonal section of a bivariate copula if and only if it satisfies the necessary conditions (Nelsen, §3.2.6).