Catalog/VC/EasyEpsilonNetLemma/Contract.lean
| 1 | import Catalog.VC.EpsilonNet.Contract |
| 2 | import Mathlib.Analysis.SpecialFunctions.Log.Basic |
| 3 | |
| 4 | namespace Catalog.VC.EasyEpsilonNetLemma |
| 5 | |
| 6 | /-- For any finite set family and `r > 1`, there exists a `(1/r)`-net of size |
| 7 | at most `r ยท ln |๐| + 1`. (Lemma 5.11) -/ |
| 8 | axiom easyEpsilonNetLemma {ฮฑ : Type*} [DecidableEq ฮฑ] [Fintype ฮฑ] |
| 9 | (๐ : Finset (Finset ฮฑ)) (h๐ : 2 โค ๐.card) {r : โ} (hr : 1 < r) : |
| 10 | โ N : Finset ฮฑ, Catalog.VC.EpsilonNet.IsEpsilonNet ๐ (1 / r) N โง |
| 11 | (N.card : โ) โค r * Real.log (๐.card : โ) + 1 |
| 12 | |
| 13 | end Catalog.VC.EasyEpsilonNetLemma |
| 14 |