Catalog/VC/EpsilonApproximation/Contract.lean
| 1 | import Mathlib.Combinatorics.SetFamily.Shatter |
| 2 | import Mathlib.Analysis.SpecialFunctions.Log.Basic |
| 3 | |
| 4 | namespace Catalog.VC.EpsilonApproximation |
| 5 | |
| 6 | variable {α : Type*} [DecidableEq α] [Fintype α] |
| 7 | |
| 8 | /-- `Y` is an `ε`-approximation for set family `𝒜` on finite ground set `α`. |
| 9 | The sample density of every `S ∈ 𝒜` in `Y` approximates its true density: |
| 10 | `| |S ∩ Y| / |Y| − |S| / |α| | ≤ ε`. -/ |
| 11 | def IsEpsilonApprox (𝒜 : Finset (Finset α)) (ε : ℝ) (Y : Finset α) : Prop := |
| 12 | ∀ S ∈ 𝒜, |((S ∩ Y).card : ℝ) / Y.card - (S.card : ℝ) / Fintype.card α| ≤ ε |
| 13 | |
| 14 | end Catalog.VC.EpsilonApproximation |
| 15 |