← Copula mathematical handbook

Extremal copulas with a prescribed diagonal section

Let δ be a diagonal function (IsDiagonalFunction) and write δ̂ t = t - δ t (diagGap). This file collects the order-theoretic facts about the set of copulas with diagonal section δ (Nelsen, An Introduction to Copulas, 2nd ed., §3.2.6; Fredricks and Nelsen, Copulas constructed from diagonal sections, 1997; Fredricks and Nelsen, The Bertino family of copulas, 2002). Upper bounds for arbitrary (non-exchangeable) copulas and quasi-copulas with diagonal δ are in Copula.Diagonal.UpperBound.

• cdf_add_cdf_swap_le: C(u,v) + C(v,u) ≤ δ(u) + δ(v) for every copula.
• isExchangeable_diagonalCopula, cdf_le_diagonalCopula: the Fredricks–Nelsen copula K_δ(u,v) = min(u, v, (δ u + δ v)/2) is exchangeable and is the pointwise largest exchangeable copula with diagonal δ.
• bertinoCopula_lt_diagonalCopula, bertinoCopula_eq_diagonalCopula_iff: if δ ≠ id, the Bertino copula and the Fredricks–Nelsen copula differ; hence diagonal_determines_copula_iff: a diagonal determines its copula uniquely if and only if it is the identity, i.e. the copula is M.

The Fredricks–Nelsen copula is the largest exchangeable one

theorem ProbabilityTheory.Copula.cdf_add_cdf_swap_le (C : Copula 2) (u v : ↑unitInterval) : C.cdf ![u, v] + C.cdf ![v, u] ≤ C.diagonal u + C.diagonal v

The increment over the diagonal square [u ∧ v, u ∨ v]²: for every bivariate copula, C(u,v) + C(v,u) ≤ δ_C(u) + δ_C(v).

theorem ProbabilityTheory.Copula.diagKernel_comm {δ : ↑unitInterval → ℝ} (u v : ↑unitInterval) : diagKernel δ u v = diagKernel δ v u

The Fredricks–Nelsen kernel is symmetric.

@[simp]

theorem ProbabilityTheory.Copula.cdf_diagonalCopula_two {δ : ↑unitInterval → ℝ} (hδ : IsDiagonalFunction δ) (u v : ↑unitInterval) : (diagonalCopula δ hδ).cdf ![u, v] = diagKernel δ u v

theorem ProbabilityTheory.Copula.isExchangeable_diagonalCopula {δ : ↑unitInterval → ℝ} (hδ : IsDiagonalFunction δ) : (diagonalCopula δ hδ).IsExchangeable

The Fredricks–Nelsen copula K_δ is exchangeable.

theorem ProbabilityTheory.Copula.cdf_le_diagonalCopula {δ : ↑unitInterval → ℝ} (hδ : IsDiagonalFunction δ) {C : Copula 2} (hC : C.IsExchangeable) (hd : ∀ (t : ↑unitInterval), C.diagonal t = δ t) (u v : ↑unitInterval) : C.cdf ![u, v] ≤ (diagonalCopula δ hδ).cdf ![u, v]

K_δ is the largest exchangeable copula with diagonal δ (Fredricks–Nelsen 1997): every exchangeable copula with diagonal section δ lies below K_δ(u,v) = min(u, v, (δ u + δ v)/2).

theorem ProbabilityTheory.Copula.lowerOrthantLE_diagonalCopula {δ : ↑unitInterval → ℝ} (hδ : IsDiagonalFunction δ) {C : Copula 2} (hC : C.IsExchangeable) (hd : ∀ (t : ↑unitInterval), C.diagonal t = δ t) : C.LowerOrthantLE (diagonalCopula δ hδ)

K_δ dominates every exchangeable copula with diagonal δ in the lower orthant order.

theorem ProbabilityTheory.Copula.bertino_le_cdf_le_diagonalCopula {δ : ↑unitInterval → ℝ} (hδ : IsDiagonalFunction δ) {C : Copula 2} (hC : C.IsExchangeable) (hd : ∀ (t : ↑unitInterval), C.diagonal t = δ t) (u v : ↑unitInterval) : (bertinoCopula δ hδ).cdf ![u, v] ≤ C.cdf ![u, v] ∧ C.cdf ![u, v] ≤ (diagonalCopula δ hδ).cdf ![u, v]

Every exchangeable copula with diagonal δ lies between the Bertino copula B_δ and the Fredricks–Nelsen copula K_δ; both bounds are exchangeable copulas with diagonal δ.

Uniqueness: only the identity diagonal determines its copula

theorem ProbabilityTheory.Copula.bertinoCopula_lt_diagonalCopula {δ : ↑unitInterval → ℝ} (hδ : IsDiagonalFunction δ) (hne : ∃ (t : ↑unitInterval), δ t ≠ ↑t) : ∃ (u : ↑unitInterval) (v : ↑unitInterval), (bertinoCopula δ hδ).cdf ![u, v] < (diagonalCopula δ hδ).cdf ![u, v]

If δ is not the identity, the Bertino copula lies strictly below the Fredricks–Nelsen copula at some point.

theorem ProbabilityTheory.Copula.bertinoCopula_eq_diagonalCopula_iff {δ : ↑unitInterval → ℝ} (hδ : IsDiagonalFunction δ) : bertinoCopula δ hδ = diagonalCopula δ hδ ↔ ∀ (t : ↑unitInterval), δ t = ↑t

The Bertino copula and the Fredricks–Nelsen copula of δ coincide if and only if δ is the identity (in which case both are M).

theorem ProbabilityTheory.Copula.diagonal_determines_copula_iff {δ : ↑unitInterval → ℝ} (hδ : IsDiagonalFunction δ) : (∀ (C D : Copula 2), (∀ (t : ↑unitInterval), C.diagonal t = δ t) → (∀ (t : ↑unitInterval), D.diagonal t = δ t) → C = D) ↔ ∀ (t : ↑unitInterval), δ t = ↑t

A diagonal section determines its copula if and only if it is the identity: for a diagonal function δ, all copulas with diagonal δ coincide exactly when δ(t) = t for all t (and then the copula is M). In particular the diagonal of W does not determine W.