Theorem 19.4: for integer c ≥ 2 and any learning rule, some distribution on [0,1]^d × {0,1} with c-Lipschitz η and Bayes error 0 forces expected error ≥ 1/4 when 2m ≤ (c+1)^d

Proved

UnderstandingML.curse_of_dimensionality

by naimengye · Sep 24, 2026 · Mathlib 0df444a (Lean v4.33.1)

curse-of-dimensionalitylower-boundnearest-neighborno-free-lunch

Theorem 19.4. For any $c > 1$ , and every learning rule, $L$ , there exists a distribution over $[0,1]^d \times \{0,1\}$ , such that $\eta(x)$ is $c$ -Lipschitz, the Bayes error of the distribution is $0$ , but for sample sizes $m \le (c+1)^d/2$ , the true error of the rule $L$ is greater than $1/4$ .

As the proof gives it (the grid $G^d_c$ with spacing $1/c$ and Theorem 5.1): $c \ge 2$ is an integer, the sample size $m$ with $2m \le (c+1)^d$ is fixed before the distribution, and the true error of $L$ is at least $1/4$ in expectation over $S \sim D^m$ (Equation (5.2) of the proof of Theorem 5.1).

Preamble

import Definitions.Def_UnderstandingML_NearestNeighbor

open MeasureTheory

Formal statement

namespace UnderstandingML

/-- **Theorem 19.4** (p. 263). For any `c > 1` and every learning rule `L`, there exists a
distribution over `[0,1]^d × {0,1}` such that `η(x)` is `c`-Lipschitz, the Bayes error of the
distribution is `0`, but for sample sizes `m ≤ (c+1)^d / 2` the true error of the rule `L` is
greater than `1/4`.
As the proof (via Theorem 5.1) gives it: `c ≥ 2` is an integer (the grid has spacing `1/c`),
the sample size `m` is fixed first, and the true error is at least `1/4` in expectation over
`S ∼ D^m`. -/
theorem curse_of_dimensionality (d c : ℕ) (hc : 2 ≤ c)
    (L : Learner (cube d × Bool) (cube d → Bool)) (m : ℕ) (hm : 2 * m ≤ (c + 1) ^ d) :
    ∃ (DX : Measure (cube d)) (η : cube d → ℝ), IsProbabilityMeasure DX ∧
      LipschitzWith c η ∧ (∀ x, η x ∈ Set.Icc (0 : ℝ) 1) ∧
      risk loss01 (condLaw DX η) (bayesRule η) = 0 ∧
      1 / 4 ≤ ∫ S, risk loss01 (condLaw DX η) (L m S) ∂(iidLaw (condLaw DX η) m) := by sorry

end UnderstandingML

Source

Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press 2014, doi:10.1017/CBO9781107298019, §19.2.2 p. 263, Theorem 19.4 with its proof (via Theorem 5.1)

Human review

Endorsed by Shuze Chen · Sep 25, 2026
Confirmed by the moderator at approval.
Endorsed by naimengye · Sep 25, 2026
Confirmed by the mission captain (proposal self-audit).

View graph