Catalog.VC.UnitDistanceGraphEdges
Lemma
For a set system \((X, \mathcal{S})\), the unit distance graph \(\mathrm{UD}(\mathcal{S})\) has vertex set \(\mathcal{S}\) and an edge \(\{S, S'\}\) whenever \(|S \mathbin{\triangle} S'| = 1\).
If \(\mathcal{S}\) is a set system of VC-dimension (Definition VCDimension) \(d_0\) on a finite set \(X\), then \(\mathrm{UD}(\mathcal{S})\) has at most \(d_0 \, |\mathcal{S}|\) edges.
Review notes
Matoušek Lemma 5.15.
The unit distance graph \(\mathrm{UD}(\mathcal{A})\) has vertex set \(\mathcal{A}\) and an edge \(\{S, S'\}\) when \(|S \triangle S'| = 1\), i.e. the two sets differ by exactly one element.
The Lean statement counts ordered pairs via Finset.offDiag
and symmDiff, so the bound is \(2 d_0 |\mathcal{A}|\) (each
undirected edge counted twice).
The proof is by induction on \(|X|\) and \(d_0\). Fix \(x \in X\), define \(\mathcal{S}_1 = \mathcal{S}|_{X \setminus \{x\}}\) (VC-dim \(\le d_0\)) and \(\mathcal{S}_2 = \{S \in \mathcal{S} : x \notin S,\; S \cup \{x\} \in \mathcal{S}\}\) (VC-dim \(\le d_0 - 1\)), then charge edges appropriately.
Catalog/VC/UnitDistanceGraphEdges/Contract.lean (full)
| 1 | import Catalog.VC.VCDimension.Contract |
| 2 | import Mathlib.Order.SymmDiff |
| 3 | |
| 4 | namespace Catalog.VC.UnitDistanceGraphEdges |
| 5 | |
| 6 | /-- The unit distance graph of a set family with VC-dimension `d₀` has at |
| 7 | most `d₀ · |𝒜|` edges. Equivalently, the number of ordered pairs |
| 8 | `(S, S')` in `𝒜` with `|S △ S'| = 1` is at most `2 · d₀ · |𝒜|`. |
| 9 | (Lemma 5.15) -/ |
| 10 | axiom unitDistEdgeBound {α : Type*} [DecidableEq α] [Fintype α] |
| 11 | (𝒜 : Finset (Finset α)) : |
| 12 | (𝒜.offDiag.filter (fun p => (symmDiff p.1 p.2).card = 1)).card |
| 13 | ≤ 2 * 𝒜.vcDim * 𝒜.card |
| 14 | |
| 15 | end Catalog.VC.UnitDistanceGraphEdges |
| 16 |