Catalog.VC.VCDimension
Definition
Let \((X, \mathcal{S})\) be a set system. A subset \(A \subseteq X\) is shattered by \(\mathcal{S}\) if \(\mathcal{S}|_A = 2^A\), that is, every subset of \(A\) is of the form \(S \cap A\) for some \(S \in \mathcal{S}\).
The VC-dimension of \(\mathcal{S}\), denoted \(\dim(\mathcal{S})\), is the supremum of the sizes of all finite shattered subsets of \(X\). Equivalently, \[\dim(\mathcal{S}) = \sup\{ m : \pi_{\mathcal{S}}(m) = 2^m \}.\]
Review notes
Both Shatters and vcDim are thin wrappers (abbrev)
around Mathlib’s Finset.Shatters and Finset.vcDim from
Mathlib.Combinatorics.SetFamily.Shatter.
Finset.Shatters\(\mathcal{A}\)s holds iff for every \(t \subseteq s\)
there exists \(u \in \mathcal{A}\) with \(s \cap u = t\). This matches
Matoušek Definition 5.8.
Finset.vcDim is defined as
\(\sup\{|s| : s \in \texttt{shatterer}(\mathcal{A})\}\), where
shatterer collects all shattered subsets. This equals
\(\sup\{m : \pi_{\mathcal{A}}(m) = 2^m\}\).
Mathlib also provides the Sauer–Shelah–Perles bound
(card_shatterer_le_sum_vcDim), which is closely related to
Catalog.VC.ShatterFunctionLemma.
Catalog/VC/VCDimension/Contract.lean (full)
| 1 | import Mathlib.Combinatorics.SetFamily.Shatter |
| 2 | |
| 3 | namespace Catalog.VC.VCDimension |
| 4 | |
| 5 | /-- A finite set `s` is shattered by family `𝒜` if every subset of `s` |
| 6 | is realized as `s ∩ S` for some `S ∈ 𝒜`. |
| 7 | Wraps Mathlib's `Finset.Shatters`. (Def 5.8) -/ |
| 8 | abbrev Shatters {α : Type*} [DecidableEq α] |
| 9 | (𝒜 : Finset (Finset α)) (s : Finset α) : Prop := |
| 10 | 𝒜.Shatters s |
| 11 | |
| 12 | /-- The VC-dimension of `𝒜`: the maximum cardinality of a set shattered |
| 13 | by `𝒜`. Equivalently, `sup { m : π_𝒜(m) = 2^m }`. |
| 14 | Wraps Mathlib's `Finset.vcDim`. (Def 5.8) -/ |
| 15 | abbrev vcDim {α : Type*} [DecidableEq α] |
| 16 | (𝒜 : Finset (Finset α)) : ℕ := |
| 17 | 𝒜.vcDim |
| 18 | |
| 19 | end Catalog.VC.VCDimension |
| 20 |