Catalog/VC/PackingLemma/Contract.lean
| 1 | import Catalog.VC.ShatterFunction.Contract |
| 2 | import Mathlib.Analysis.SpecialFunctions.Pow.Real |
| 3 | |
| 4 | namespace Catalog.VC.PackingLemma |
| 5 | |
| 6 | variable {α : Type*} [DecidableEq α] |
| 7 | |
| 8 | /-- A subfamily `𝒫` is `δ`-separated if any two distinct members have |
| 9 | symmetric difference of size strictly greater than `δ`. -/ |
| 10 | def IsSeparated (P : Finset (Finset α)) (δ : ℕ) : Prop := |
| 11 | ∀ S ∈ P, ∀ S' ∈ P, S ≠ S' → δ < (S \ S' ∪ (S' \ S)).card |
| 12 | |
| 13 | /-- Packing lemma: if the shatter function satisfies `π_𝒜(m) ≤ C · m^d` |
| 14 | and `𝒫 ⊆ 𝒜` is `δ`-separated, then `|𝒫| ≤ C' · (n/δ)^d`. |
| 15 | The constant `C'` depends only on `C` and `d`. (Lemma 5.14) -/ |
| 16 | axiom packingLemma (d : ℕ) (C : ℝ) (hC : 0 < C) : ∃ C' : ℝ, 0 < C' ∧ |
| 17 | ∀ (α : Type*) [DecidableEq α] [Fintype α] (F P : Finset (Finset α)), |
| 18 | P ⊆ F → |
| 19 | (∀ m : ℕ, (Catalog.VC.ShatterFunction.shatterFun F m : ℝ) ≤ C * (m : ℝ) ^ d) → |
| 20 | ∀ (δ : ℕ), 0 < δ → δ ≤ Fintype.card α → |
| 21 | IsSeparated P δ → |
| 22 | (P.card : ℝ) ≤ C' * ((Fintype.card α : ℝ) / δ) ^ d |
| 23 | |
| 24 | end Catalog.VC.PackingLemma |
| 25 |