Catalog/VC/ShortEdgeLemma/Contract.lean
| 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 |