Prove2Me
Navigate
DiscoverFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Lemma 29.5: if VCdim(H_bin) = d then every set shattered by the One-versus-All class H^{OvA,k}_bin has size ≤ 3kd log(kd)

Proved
UnderstandingML.ova_ndim_bound

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

natarajan-dimensionone-versus-allsauer-lemma

Lemma 29.5. If d=VCdim⁡(Hbin)d = \operatorname{VCdim}(H_{bin})d=VCdim(Hbin​) then Ndim⁡(HbinOvA,k)≤3kdlog⁡(kd)\operatorname{Ndim}(H^{OvA,k}_{bin}) \le 3kd\log(kd)Ndim(HbinOvA,k​)≤3kdlog(kd).

Formally: every set shattered by HbinOvA,kH^{OvA,k}_{bin}HbinOvA,k​ has size at most 3kdlog⁡(kd)3kd\log(kd)3kdlog(kd) (natural logarithm; the bound is 000 when kd≤1kd \le 1kd≤1). The book's step ∣(Hbin)C∣≤∣C∣d|(H_{bin})_C| \le |C|^d∣(Hbin​)C​∣≤∣C∣d fails for small ∣C∣|C|∣C∣ (for ∣C∣=2|C| = 2∣C∣=2, d=1d = 1d=1), but the statement is true: the exact Sauer count 2c≤(∑i≤d(ci))k2^c \le (\sum_{i \le d}\binom{c}{i})^k2c≤(∑i≤d​(ic​))k gives it for every (k,d)(k, d)(k,d) except (2,1)(2, 1)(2,1) and (3,1)(3, 1)(3,1). In those two cases, group a shattered set by the label pair {f0(x),f1(x)}\{f_0(x), f_1(x)\}{f0​(x),f1​(x)}. On pairs {0,b}\{0, b\}{0,b} the realized sets are hb∖h0h_b \setminus h_0hb​∖h0​, and on pairs {a,b}\{a, b\}{a,b} with a≥1a \ge 1a≥1 they are hah_aha​ itself. The class {B∖A:A,B∈Hbin}\{B \setminus A : A, B \in H_{bin}\}{B∖A:A,B∈Hbin​} cannot shatter 555 points: on them ∣Hbin∣≤6|H_{bin}| \le 6∣Hbin​∣≤6, and the 666 pairs A=BA = BA=B all give ∅\emptyset∅, so at most 31<3231 < 3231<32 sets. Hence ∣C∣≤4<4.16|C| \le 4 < 4.16∣C∣≤4<4.16 for k=2k = 2k=2 and ∣C∣≤4+4+1=9<9.89|C| \le 4 + 4 + 1 = 9 < 9.89∣C∣≤4+4+1=9<9.89 for k=3k = 3k=3.

Preamble
import Definitions.Def_UnderstandingML_MulticlassLearnability

open MeasureTheory
open scoped InnerProductSpace
Formal statement
namespace UnderstandingML

/-- **Lemma 29.5** (p. 404). If `d = VCdim(H_bin)` then `Ndim(H^{OvA,k}_bin) ≤ 3kd log(kd)`, stated
for every shattered set. The book's proof uses `|(H_bin)_C| ≤ |C|^d`, which fails for small `|C|`
(`|C| = 2`, `d = 1`). The statement is nevertheless true: the exact Sauer count
`2^c ≤ (∑_{i ≤ d} (c choose i))^k` gives it except at `(k, d) = (2, 1), (3, 1)`. There, grouping a
shattered set by the label pair `{f₀(x), f₁(x)}` bounds it by `4` and by `4 + 4 + 1 = 9`,
because `{B \ A : A, B ∈ H_bin}` has at most `31` traces on `5` points. -/
theorem ova_ndim_bound {X : Type*} (Hbin : Set (X → Bool)) (d : ℕ) (hd : vcDim Hbin = d)
    (k : ℕ) [NeZero k] (C : Finset X) (hC : NShatters (ovaClass Hbin k) C) :
    (C.card : ℝ) ≤ 3 * k * d * Real.log (k * d) := 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, §29.3.1 pp. 404-405, Lemma 29.5 with its proof
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

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me