Catalog.VC.EpsilonApproximationBound
Lemma
Let \(X\) be a finite set of \(n\) points, let \(\mathcal{S}\) be a set system of VC-dimension (Definition VCDimension) at most \(d\) on \(X\), and let \(r \ge 2\). Then there exists a \(\frac{1}{r}\)-approximation (Definition EpsilonApproximation) \(Y\) for \((X, \mathcal{S})\) of size \[|Y| \le C(d)\, r^2 \log r,\] where \(C(d)\) is a constant depending only on \(d\).
Review notes
Matoušek Lemma 5.13.
The constant \(C\) is quantified before the ground-set type \(\alpha\), ensuring it depends only on the VC-dimension bound \(d\).
The proof uses repeated halving with random coloring (the “random coloring
lemma”): starting from \(Y_0 = X\), each step halves \(|Y_i|\) while
accumulating error \(\varepsilon_i = O(\sqrt{\ln n_i / n_i})\) using
Catalog.VC.ShatterFunctionLemma. Stopping at \(|Y_\ell| < C r^2 \log r\)
gives cumulative error \(\le 1/r\).
The random coloring lemma itself is not a separate catalog entry; it will be
proved as a helper within the Full.lean of this entry during
Phase 5.
Catalog/VC/EpsilonApproximationBound/Contract.lean (full)
| 1 | import Catalog.VC.VCDimension.Contract |
| 2 | import Catalog.VC.EpsilonApproximation.Contract |
| 3 | import Mathlib.Analysis.SpecialFunctions.Log.Basic |
| 4 | import Mathlib.Analysis.SpecialFunctions.Pow.Real |
| 5 | |
| 6 | namespace Catalog.VC.EpsilonApproximationBound |
| 7 | |
| 8 | /-- For any finite set family of VC-dimension at most `d`, and `r ≥ 2`, |
| 9 | there exists a `(1/r)`-approximation of size `O(r² log r)`. |
| 10 | The constant `C` depends only on `d`. (Lemma 5.13) -/ |
| 11 | axiom epsilonApproxBound (d : ℕ) : ∃ C : ℝ, 0 < C ∧ |
| 12 | ∀ (α : Type*) [DecidableEq α] [Fintype α] (𝒜 : Finset (Finset α)), |
| 13 | 𝒜.vcDim ≤ d → |
| 14 | ∀ (r : ℝ), 2 ≤ r → |
| 15 | ∃ Y : Finset α, Catalog.VC.EpsilonApproximation.IsEpsilonApprox 𝒜 (1 / r) Y ∧ |
| 16 | (Y.card : ℝ) ≤ C * r ^ 2 * Real.log r |
| 17 | |
| 18 | end Catalog.VC.EpsilonApproximationBound |
| 19 |