Catalog.VC.ShortEdgeLemma
Lemma
Let \((X, \mathcal{S})\) be a set system on an \(n\)-point set \(X\) with dual shatter function (Definition DualShatterFunction) \(\pi_{\mathcal{S}}^*(m) \le C m^d\) for all \(m\), where \(C\) and \(d > 1\) are constants. A set \(S \in \mathcal{S}\) crosses an edge \(\{u,v\}\) of a graph on \(X\) if \(|S \cap \{u,v\}| = 1\).
Then for any multiset \(Q\) of sets from \(\mathcal{S}\), there exist distinct points \(x, y \in X\) such that the number of sets of \(Q\) crossing \(\{x, y\}\) is at most \[C_2 \, \frac{|Q|}{n^{1/d}},\] where \(C_2\) depends only on \(C\) and \(d\).
Review notes
Matoušek Lemma 5.18.
crossingNumber counts the sets in \(Q\) that contain exactly one of
\(x, y\). The source allows \(Q\) to be a multiset; we use a Finset
(no duplicate sets). This is a slight weakening but suffices for all
downstream applications in the catalog.
The constant \(C_2\) depends only on \(C\) and \(d\) (quantified before \(\alpha\)). The hypothesis \(2 \le |\alpha|\) ensures two distinct points exist.
Proof outline. Form the dual set system
\(\mathcal{D} = \{D_x : x \in X\}\) on ground set \(Q\), where
\(D_x = \{S \in Q : x \in S\}\). Then \(|D_x \triangle D_y|\) equals the
crossing number of \(\{x, y\}\). The dual shatter function bound implies
\(\pi_{\mathcal{D}}(m) \le C m^d\). Apply Catalog.VC.PackingLemma: if all
pairwise symmetric differences are \(\ge \delta\), then
\(n = O((|Q|/\delta)^d)\), giving \(\delta = O(|Q| / n^{1/d})\). The minimum
pairwise distance is at most \(\delta\).
Catalog/VC/ShortEdgeLemma/Contract.lean (full)
| 1 | import Catalog.VC.DualShatterFunction.Contract |
| 2 | import Mathlib.Analysis.SpecialFunctions.Pow.Real |
| 3 | |
| 4 | namespace Catalog.VC.ShortEdgeLemma |
| 5 | |
| 6 | universe u |
| 7 | |
| 8 | variable {α : Type*} [DecidableEq α] |
| 9 | |
| 10 | /-- The crossing number of an edge `{x, y}` by a subfamily `Q`: the number |
| 11 | of sets in `Q` that contain exactly one of `x, y`. -/ |
| 12 | abbrev crossingNumber (Q : Finset (Finset α)) (x y : α) : ℕ := |
| 13 | (Q.filter (fun S => (x ∈ S ∧ y ∉ S) ∨ (x ∉ S ∧ y ∈ S))).card |
| 14 | |
| 15 | /-- Short edge lemma: if the dual shatter function satisfies |
| 16 | `π*_𝒜(m) ≤ C · m^d` with `d > 1`, then for any subfamily `Q ⊆ 𝒜` |
| 17 | there exist distinct points `x, y` with crossing number at most |
| 18 | `C₂ · |Q| / n^{1/d}`. (Lemma 5.18) -/ |
| 19 | axiom shortEdgeLemma (d : ℕ) (C : ℝ) (hd : 1 < d) (hC : 0 < C) : |
| 20 | ∃ C₂ : ℝ, 0 < C₂ ∧ |
| 21 | ∀ (α : Type u) [DecidableEq α] [Fintype α] (𝒜 : Finset (Finset α)), |
| 22 | (∀ m : ℕ, (Catalog.VC.DualShatterFunction.dualShatterFun 𝒜 m : ℝ) ≤ C * (m : ℝ) ^ d) → |
| 23 | 2 ≤ Fintype.card α → |
| 24 | ∀ (Q : Finset (Finset α)), Q ⊆ 𝒜 → |
| 25 | ∃ x y : α, x ≠ y ∧ |
| 26 | ((Q.filter (fun S => (x ∈ S ∧ y ∉ S) ∨ (x ∉ S ∧ y ∈ S))).card : ℝ) ≤ |
| 27 | C₂ * (Q.card : ℝ) / |
| 28 | (Fintype.card α : ℝ) ^ ((1 : ℝ) / d) |
| 29 | |
| 30 | end Catalog.VC.ShortEdgeLemma |
| 31 |