← Copula mathematical handbook

The sharp population bounds for Hoeffding's D

The pointwise Bernoulli covariance bound (C(u,v) - uv)² ≤ u(1-u) v(1-v) gives 0 ≤ D ≤ 1/30 for Hoeffding's D = ∫ (C - Π)² dC; the upper bound is attained at M and W (hoeffdingD_comonotonic, hoeffdingD_countermonotonic), so 30 D ∈ [0,1].

theorem ProbabilityTheory.Copula.cdfDeviation_sq_le (C : Copula 2) (x : Fin 2 → ↑unitInterval) : C.cdfDeviation x ^ 2 ≤ ↑(x 0) * (1 - ↑(x 0)) * (↑(x 1) * (1 - ↑(x 1)))

The Bernoulli covariance bound for a copula discrepancy.

theorem ProbabilityTheory.Copula.hoeffdingD_le (C : Copula 2) : C.hoeffdingD ≤ 1 / 30

theorem ProbabilityTheory.Copula.hoeffdingD_mem_Icc (C : Copula 2) : C.hoeffdingD ∈ Set.Icc 0 (1 / 30)

theorem ProbabilityTheory.Copula.hoeffdingDNormalized_mem_Icc (C : Copula 2) : C.hoeffdingDNormalized ∈ Set.Icc 0 1