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