Catalog.VC.DualShatterFunction
Definition
Let \((X, \mathcal{S})\) be a set system. The dual shatter function \(\pi_{\mathcal{S}}^* \colon \mathbb{N} \to \mathbb{N}\) is defined by \[\pi_{\mathcal{S}}^*(m) = \max_{\mathcal{Y} \subseteq \mathcal{S},\; |\mathcal{Y}| = m} \bigl|\bigl\{ \{S \in \mathcal{Y} : x \in S\} : x \in X \bigr\}\bigr|.\] Equivalently, \(\pi_{\mathcal{S}}^*(m)\) is the maximum number of nonempty cells in the Venn diagram of \(m\) sets chosen from \(\mathcal{S}\).
Review notes
The dual shatter function from Matoušek Definition 5.2.
atomMap assigns to each point \(x \in \alpha\) the subfamily
\(\{S \in \mathcal{Y} : x \in S\}\). Two points \(x, y\) lie in the same
Venn-diagram cell iff \(\texttt{atomMap}\;\mathcal{Y}\;x =
\texttt{atomMap}\;\mathcal{Y}\;y\).
dualShatterFun maximizes the number of distinct atom maps over all
\(m\)-element subfamilies \(\mathcal{Y} \subseteq \mathcal{A}\). The powerset
of \(\mathcal{A}\) is enumerated via Finset.powerset.
The source describes the dual shatter function in terms of equivalence
classes on \(X\). The Lean encoding counts distinct images of atomMap
instead, which is equivalent.
Catalog/VC/DualShatterFunction/Contract.lean (full)
| 1 | import Mathlib.Combinatorics.SetFamily.Shatter |
| 2 | |
| 3 | namespace Catalog.VC.DualShatterFunction |
| 4 | |
| 5 | variable {α : Type*} [DecidableEq α] |
| 6 | |
| 7 | /-- The atom map of a subfamily `𝒴` at point `x`: the set of members |
| 8 | of `𝒴` that contain `x`. Two points `x, y` have the same atom map |
| 9 | iff they belong to exactly the same sets of `𝒴`. -/ |
| 10 | def atomMap (𝒴 : Finset (Finset α)) (x : α) : Finset (Finset α) := |
| 11 | 𝒴.filter (x ∈ ·) |
| 12 | |
| 13 | /-- The dual shatter function `π*_𝒜(m)`: the maximum number of distinct |
| 14 | atom types induced by any `m`-element subfamily of `𝒜`. |
| 15 | Equivalently, the maximum number of nonempty cells in the Venn diagram |
| 16 | of `m` sets chosen from `𝒜`. (Def 5.2) -/ |
| 17 | def dualShatterFun [Fintype α] (𝒜 : Finset (Finset α)) (m : ℕ) : ℕ := |
| 18 | (𝒜.powerset.filter (fun 𝒴 => 𝒴.card = m)).sup |
| 19 | (fun 𝒴 => (Finset.univ.image (atomMap 𝒴)).card) |
| 20 | |
| 21 | end Catalog.VC.DualShatterFunction |
| 22 |