Catalog.VC.EpsilonApproximation
Definition
Let \((X, \mathcal{S})\) be a set system with \(X\) finite. A subset \(Y \subseteq X\) is an \(\varepsilon\)-approximation for \((X, \mathcal{S})\) if \[\left| \frac{|Y \cap S|}{|Y|} - \frac{|S|}{|X|} \right| \le \varepsilon\] for all \(S \in \mathcal{S}\).
Review notes
The \(\varepsilon\)-approximation definition from Matoušek Section 5.2 (page 148).
An \(\varepsilon\)-approximation \(Y\) ensures that for every set \(S\) in the family, the sample fraction \(|S \cap Y|/|Y|\) is within \(\varepsilon\) of the true density \(|S|/|\alpha|\).
The source notes that every \(\varepsilon\)-approximation is also an \(\varepsilon\)-net. This is not part of the contract but follows immediately from the definitions.
Division by zero (\(|Y| = 0\) or \(|\alpha| = 0\)) produces \(0\) in Lean’s division on \(\mathbb{R}\). Theorems using this definition will carry appropriate positivity hypotheses.
Catalog/VC/EpsilonApproximation/Contract.lean (full)
| 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 |