Catalog.VC.EpsilonNet
Definition
Let \((X, \mathcal{S})\) be a set system and \(\mu\) a probability measure on \(X\). A subset \(N \subseteq X\) is an \(\varepsilon\)-net for \((X, \mathcal{S})\) with respect to \(\mu\) if \(N \cap S \ne \emptyset\) for every \(S \in \mathcal{S}\) with \(\mu(S) \ge \varepsilon\).
When \(X\) is finite and \(\mu\) is the counting measure (\(\mu(A) = |A|/|X|\)), this says that \(N\) intersects every set \(S \in \mathcal{S}\) with \(|S| \ge \varepsilon |X|\).
Review notes
The \(\varepsilon\)-net definition from Matoušek Section 5.2 (page 147).
The source defines \(\varepsilon\)-nets with respect to a general probability measure \(\mu\). We specialize to the uniform distribution on a finite type \(\alpha\): a set \(S\) has density \(|S|/|\alpha|\), so \(\mu(S) \ge \varepsilon\) becomes \(\varepsilon \cdot |\alpha| \le |S|\).
This finite-uniform reformulation is faithful only when the ground type is
nonempty, as in the source probability-space setting. On \(\alpha = \emptyset\),
the heavy-set test degenerates to \(0 \le |S|\), so the empty set counts as
heavy and Catalog.VC.EpsilonNet.IsEpsilonNet asks for an impossible
nonempty intersection with \(\emptyset\). Downstream entries that assert the
existence of \(\varepsilon\)-nets must therefore exclude this pathology, either
by assuming [Nonempty α] or by imposing hypotheses that already rule
out the empty type.
The condition \(N \cap S \ne \emptyset\) is encoded as
(N \(\cap\) S).Nonempty, which is Finset.Nonempty.
The Catalog.VC.EpsilonNetTheorem will quantify over all finite types to
recover the generality of the source statement.
Catalog/VC/EpsilonNet/Contract.lean (full)
| 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 |