Catalog.VC.ShatterFunctionLemma
Lemma
For any set system \(\mathcal{S}\) of VC-dimension at most \(d\) (Definition VCDimension), the primal shatter function (Definition ShatterFunction) satisfies \[\pi_{\mathcal{S}}(m) \le \Phi_d(m) \quad \text{for all } m,\] where \[\Phi_d(m) = \binom{m}{0} + \binom{m}{1} + \cdots + \binom{m}{d}.\]
Review notes
Matoušek Lemma 5.9 (the Sauer–Shelah–Perles lemma).
The auxiliary definition binomialSum encodes \(\Phi_d(m) =
\sum_{k=0}^{d} \binom{m}{k}\), using Finset.range and
Nat.choose.
Mathlib already has the closely related
Finset.card_shatterer_le_sum_vcDim, which bounds
\(|\texttt{shatterer}(\mathcal{A})| \le \Phi_d(n)\) where \(n = |\alpha|\).
Our statement bounds the shatter function \(\pi_{\mathcal{A}}(m) \le \Phi_d(m)\)
for each \(m\), which follows by restricting \(\mathcal{A}\) to traces on an
\(m\)-element subset and applying the Mathlib bound.
The contract uses Catalog.VC.ShatterFunction.shatterFun for \(\pi\) and
Finset.vcDim (via Catalog.VC.VCDimension) for the VC-dimension.
Catalog/VC/ShatterFunctionLemma/Contract.lean (full)
| 1 | import Catalog.VC.ShatterFunction.Contract |
| 2 | import Catalog.VC.VCDimension.Contract |
| 3 | |
| 4 | namespace Catalog.VC.ShatterFunctionLemma |
| 5 | |
| 6 | /-- The binomial sum `Φ_d(m) = ∑_{k=0}^{d} C(m, k)`. Upper bound for the |
| 7 | shatter function of a family with VC-dimension at most `d`. -/ |
| 8 | def binomialSum (d m : ℕ) : ℕ := |
| 9 | (Finset.range (d + 1)).sum (fun k => m.choose k) |
| 10 | |
| 11 | /-- The shatter function of a family with VC-dimension at most `d` is bounded |
| 12 | by the binomial sum: `π_𝒜(m) ≤ Φ_d(m)` for all `m`. (Lemma 5.9) -/ |
| 13 | axiom shatterFunctionLemma {α : Type*} [DecidableEq α] [Fintype α] |
| 14 | (𝒜 : Finset (Finset α)) {d : ℕ} (hd : 𝒜.vcDim ≤ d) (m : ℕ) : |
| 15 | Catalog.VC.ShatterFunction.shatterFun 𝒜 m ≤ binomialSum d m |
| 16 | |
| 17 | end Catalog.VC.ShatterFunctionLemma |
| 18 |