Haussler's packing lemma

This file proves Haussler's packing lemma, which is the statement that an ε-separated set family of VC dimension at most d over finitely many elements has size at most (Cε⁻¹) ^ d for some absolute constant C.

References

• Sphere Packing Numbers for Subsets of the Boolean n-Cube with Bounded Vapnik-Chervonenkis Dimension, David Haussler
• Write-up by Thomas Bloom: http://www.thomasbloom.org/notes/vc.html

theorem SetFamily.haussler_packing {α : Type u_1} [Fintype α] {𝓕 : Finset (Set α)} {k d : ℕ} (isNIPWith_𝓕 : IsNIPWith d ↑𝓕) (isSeparated_𝓕 : Metric.IsSeparated (↑k / ↑(Fintype.card α)) ((fun (A : Set α) => WithLp.toLp 1 (A.indicator 1)) '' ↑𝓕)) (hk : k ≤ Fintype.card α) : ↑𝓕.card ≤ Real.exp 1 * (↑d + 1) * (2 * Real.exp 1 * (↑(Fintype.card α) + 1) / (↑k + 2 * ↑d + 2))

The Haussler packing lemma