Catalog.VC.PackingLemma
Lemma
Let \(d > 1\) and \(C\) be constants, and let \((X, \mathcal{S})\) be a set system on an \(n\)-point set whose primal shatter function (Definition ShatterFunction) satisfies \(\pi_{\mathcal{S}}(m) \le C m^d\) for all \(m = 1, 2, \ldots, n\). Let \(\delta\) be an integer, \(1 \le \delta \le n\), and let \(\mathcal{P} \subseteq \mathcal{S}\) be \(\delta\)-separated: any two distinct sets of \(\mathcal{P}\) satisfy \(|S_1 \mathbin{\triangle} S_2| > \delta\). Then \[|\mathcal{P}| = O\!\left(\left(\frac{n}{\delta}\right)^{\!d}\right).\]
Review notes
Matoušek Lemma 5.14 (Haussler’s packing lemma).
IsSeparated encodes \(\delta\)-separation: any two distinct members
\(S, S'\) satisfy \(|S \triangle S'| > \delta\). The symmetric difference is
written as \(S \setminus S' \cup S' \setminus S\) rather than using
symmDiff, to avoid an extra import.
The hypothesis uses the shatter function bound
\(\pi_{\mathcal{A}}(m) \le C m^d\) rather than a VC-dimension bound. This is
more general: the VC-dimension bound implies the shatter function bound via
Catalog.VC.ShatterFunctionLemma, but the packing lemma applies whenever
the shatter function has polynomial growth.
The constant \(C'\) depends only on \(C\) and \(d\) (quantified before \(\alpha\)).
The proof uses a probabilistic argument: sample a random \(s\)-element subset
\(A\), form the weighted unit distance graph of the traces on \(A\), then
combine upper and lower bounds on the total edge weight using
Catalog.VC.UnitDistanceGraphEdges.
Catalog/VC/PackingLemma/Contract.lean (full)
| 1 | import Catalog.VC.ShatterFunction.Contract |
| 2 | import Mathlib.Analysis.SpecialFunctions.Pow.Real |
| 3 | |
| 4 | namespace Catalog.VC.PackingLemma |
| 5 | |
| 6 | variable {α : Type*} [DecidableEq α] |
| 7 | |
| 8 | /-- A subfamily `𝒫` is `δ`-separated if any two distinct members have |
| 9 | symmetric difference of size strictly greater than `δ`. -/ |
| 10 | def IsSeparated (P : Finset (Finset α)) (δ : ℕ) : Prop := |
| 11 | ∀ S ∈ P, ∀ S' ∈ P, S ≠ S' → δ < (S \ S' ∪ (S' \ S)).card |
| 12 | |
| 13 | /-- Packing lemma: if the shatter function satisfies `π_𝒜(m) ≤ C · m^d` |
| 14 | and `𝒫 ⊆ 𝒜` is `δ`-separated, then `|𝒫| ≤ C' · (n/δ)^d`. |
| 15 | The constant `C'` depends only on `C` and `d`. (Lemma 5.14) -/ |
| 16 | axiom packingLemma (d : ℕ) (C : ℝ) (hC : 0 < C) : ∃ C' : ℝ, 0 < C' ∧ |
| 17 | ∀ (α : Type*) [DecidableEq α] [Fintype α] (F P : Finset (Finset α)), |
| 18 | P ⊆ F → |
| 19 | (∀ m : ℕ, (Catalog.VC.ShatterFunction.shatterFun F m : ℝ) ≤ C * (m : ℝ) ^ d) → |
| 20 | ∀ (δ : ℕ), 0 < δ → δ ≤ Fintype.card α → |
| 21 | IsSeparated P δ → |
| 22 | (P.card : ℝ) ≤ C' * ((Fintype.card α : ℝ) / δ) ^ d |
| 23 | |
| 24 | end Catalog.VC.PackingLemma |
| 25 |