← Copula mathematical handbook

Fréchet–Hoeffding bounds

Every copula lies between the lower bound max 0 (∑ i, u i - d + 1) and the minimum coordinate. The upper bound uses an infimum in the unit interval, so its value in dimension zero is one. These are bounds on the CDF; the lower bound does not in general define a copula in dimensions greater than two.

theorem ProbabilityTheory.Copula.sum_sub_dim_add_one_le_cdf {d : ℕ} (C : Copula d) (u : Fin d → ↑unitInterval) : ∑ i : Fin d, ↑(u i) - ↑d + 1 ≤ C.cdf u

The untruncated lower Fréchet–Hoeffding bound, obtained from the union bound.

theorem ProbabilityTheory.Copula.frechet_lower_le_cdf {d : ℕ} (C : Copula d) (u : Fin d → ↑unitInterval) : max 0 (∑ i : Fin d, ↑(u i) - ↑d + 1) ≤ C.cdf u

The lower Fréchet–Hoeffding bound, including dimension zero.

theorem ProbabilityTheory.Copula.cdf_le_frechet_upper {d : ℕ} (C : Copula d) (u : Fin d → ↑unitInterval) : C.cdf u ≤ ↑(⨅ (i : Fin d), u i)

The upper Fréchet–Hoeffding bound, with the empty infimum equal to one.