Catalog/VC/EpsilonNet/Contract.lean
| 1 | import Mathlib.Combinatorics.SetFamily.Shatter |
| 2 | import Mathlib.Analysis.SpecialFunctions.Log.Basic |
| 3 | |
| 4 | namespace Catalog.VC.EpsilonNet |
| 5 | |
| 6 | variable {α : Type*} [DecidableEq α] [Fintype α] |
| 7 | |
| 8 | /-- `N` is an `ε`-net for set family `𝒜` under the uniform distribution |
| 9 | on the finite ground set `α`. Every `S ∈ 𝒜` whose density |
| 10 | `|S| / |α| ≥ ε` satisfies `N ∩ S ≠ ∅`. -/ |
| 11 | def IsEpsilonNet (𝒜 : Finset (Finset α)) (ε : ℝ) (N : Finset α) : Prop := |
| 12 | ∀ S ∈ 𝒜, ε * (Fintype.card α : ℝ) ≤ (S.card : ℝ) → (N ∩ S).Nonempty |
| 13 | |
| 14 | end Catalog.VC.EpsilonNet |
| 15 |