← Copula mathematical handbook

The lower Fréchet–Hoeffding bound in dimension d

The function W_d(u) = max(0, u₁ + ⋯ + u_d - d + 1) bounds every d-copula from below (frechet_lower_le_cdf). This module records the standard facts about W_d itself (Nelsen 2006, §2.10; Durante–Sempi 2016, §1.7):

• lowerFrechetBound d is a d-quasi-copula for every d (isQuasiCopula_lowerFrechetBound), and for d = 2 it is the CDF of W (lowerFrechetBound_two);
• the W_d-volume of the cube [1/2, 1]^d equals 1 - d/2 (rectangleIncrement_lowerFrechetBound_half), which is negative for d ≥ 3; hence W_d is not d-increasing (not_isClassical_lowerFrechetBound) and no d-copula has CDF W_d (cdf_ne_lowerFrechetBound).

That W_d is nevertheless pointwise best possible (Nelsen 2006, §2.10) is proved in Copula.Multivariate.LowerBoundAttained.

noncomputable def ProbabilityTheory.Copula.lowerFrechetBound (d : ℕ) (u : Fin d → ↑unitInterval) : ℝ

The lower Fréchet–Hoeffding bound W_d(u) = max(0, ∑ uᵢ - d + 1).

Equations

• ProbabilityTheory.Copula.lowerFrechetBound d u = max 0 (∑ i : Fin d, ↑(u i) - ↑d + 1)

theorem ProbabilityTheory.Copula.lowerFrechetBound_le_cdf {d : ℕ} (C : Copula d) (u : Fin d → ↑unitInterval) : lowerFrechetBound d u ≤ C.cdf u

theorem ProbabilityTheory.Copula.lowerFrechetBound_nonneg {d : ℕ} (u : Fin d → ↑unitInterval) : 0 ≤ lowerFrechetBound d u

theorem ProbabilityTheory.Copula.lowerFrechetBound_two (u : Fin 2 → ↑unitInterval) : lowerFrechetBound 2 u = countermonotonic.cdf u

In dimension two the lower bound is the CDF of the countermonotonic copula W.

theorem ProbabilityTheory.Copula.isQuasiCopula_lowerFrechetBound (d : ℕ) : IsQuasiCopula (lowerFrechetBound d)

W_d is a quasi-copula in every dimension.

theorem ProbabilityTheory.Copula.rectangleIncrement_lowerFrechetBound_half {d : ℕ} : (rectangleIncrement (lowerFrechetBound d) (fun (x : Fin d) => unitHalf) fun (x : Fin d) => 1) = 1 - ↑d / 2

The W_d-volume of [1/2, 1]^d is 1 - d/2 (Nelsen 2006, §2.10).

theorem ProbabilityTheory.Copula.rectangleIncrement_lowerFrechetBound_neg {d : ℕ} (hd : 3 ≤ d) : (rectangleIncrement (lowerFrechetBound d) (fun (x : Fin d) => unitHalf) fun (x : Fin d) => 1) < 0

W_d is not d-increasing for d ≥ 3: the cube [1/2, 1]^d has negative volume.

theorem ProbabilityTheory.Copula.not_isClassical_lowerFrechetBound {d : ℕ} (hd : 3 ≤ d) : ¬IsClassical (lowerFrechetBound d)

For d ≥ 3, W_d violates the classical copula conditions.

theorem ProbabilityTheory.Copula.cdf_ne_lowerFrechetBound {d : ℕ} (hd : 3 ≤ d) (C : Copula d) : C.cdf ≠ lowerFrechetBound d

For d ≥ 3 no d-copula has CDF W_d (Nelsen 2006, §2.10).