Catalog.VC.ShatterFunction
Definition
Let \((X, \mathcal{S})\) be a set system, where \(\mathcal{S} \subseteq 2^X\). The primal shatter function \(\pi_{\mathcal{S}} \colon \mathbb{N} \to \mathbb{N}\) is defined by \[\pi_{\mathcal{S}}(m) = \max_{Y \subseteq X,\; |Y| = m} |\mathcal{S}|_Y|,\] where \(\mathcal{S}|_Y = \{ S \cap Y : S \in \mathcal{S} \}\) is the trace of \(\mathcal{S}\) on \(Y\).
Review notes
The primal shatter function from Matoušek Definition 5.1 is encoded as two declarations.
trace computes the trace (restriction) \(\mathcal{S}|_Y = \{S \cap Y :
S \in \mathcal{S}\}\) via Finset.image. Duplicates are collapsed
automatically by the Finset representation.
shatterFun takes the supremum of \(|\mathcal{S}|_Y|\) over all
\(Y \subseteq \alpha\) with \(|Y| = m\), using Finset.sup over
Finset.univ filtered by cardinality. The supremum over an empty
family returns \(0\), matching the convention \(\pi_{\mathcal{S}}(m) = 0\) when
\(m > |\alpha|\).
Set families are modeled as Finset (Finset \(\alpha\)) with
[DecidableEq \(\alpha\)], matching Mathlib’s VC-dimension
infrastructure in Mathlib.Combinatorics.SetFamily.Shatter.
Catalog/VC/ShatterFunction/Contract.lean (full)
| 1 | import Mathlib.Combinatorics.SetFamily.Shatter |
| 2 | |
| 3 | namespace Catalog.VC.ShatterFunction |
| 4 | |
| 5 | variable {α : Type*} [DecidableEq α] |
| 6 | |
| 7 | /-- The trace (restriction) of a set family `𝒜` on a subset `Y`: |
| 8 | the family `{ S ∩ Y | S ∈ 𝒜 }` of distinct intersections. -/ |
| 9 | def trace (𝒜 : Finset (Finset α)) (Y : Finset α) : Finset (Finset α) := |
| 10 | 𝒜.image (· ∩ Y) |
| 11 | |
| 12 | /-- The primal shatter function `π_𝒜(m)`: the maximum number of distinct |
| 13 | traces of `𝒜` on any `m`-element subset of the ground set. (Def 5.1) -/ |
| 14 | def shatterFun [Fintype α] (𝒜 : Finset (Finset α)) (m : ℕ) : ℕ := |
| 15 | (Finset.univ.filter (fun Y : Finset α => Y.card = m)).sup |
| 16 | (fun Y => (trace 𝒜 Y).card) |
| 17 | |
| 18 | end Catalog.VC.ShatterFunction |
| 19 |