Catalog/VC/EpsilonNetTheorem/Contract.lean
| 1 | import Catalog.VC.VCDimension.Contract |
| 2 | import Catalog.VC.EpsilonNet.Contract |
| 3 | import Mathlib.Analysis.SpecialFunctions.Log.Basic |
| 4 | |
| 5 | namespace Catalog.VC.EpsilonNetTheorem |
| 6 | |
| 7 | /-- For every VC-dimension bound `d`, there exists a constant `C` such that |
| 8 | any set family with VC-dimension at most `d` admits a `(1/r)`-net of size |
| 9 | at most `C · r · ln r`, for all `r ≥ 2`. (Theorem 5.12) -/ |
| 10 | axiom epsilonNetTheorem (d : ℕ) : ∃ C : ℝ, 0 < C ∧ |
| 11 | ∀ (α : Type*) [DecidableEq α] [Fintype α] [Nonempty α] (𝒜 : Finset (Finset α)), |
| 12 | 𝒜.vcDim ≤ d → |
| 13 | ∀ (r : ℝ), 2 ≤ r → |
| 14 | ∃ N : Finset α, Catalog.VC.EpsilonNet.IsEpsilonNet 𝒜 (1 / r) N ∧ |
| 15 | (N.card : ℝ) ≤ C * r * Real.log r |
| 16 | |
| 17 | end Catalog.VC.EpsilonNetTheorem |
| 18 |