Catalog/VC/ShatterFunctionLemma/Contract.lean
| 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 |