PhD: Start on Haussler's packing lemma

LeanCamCombi.lean

@@ -45,6 +45,7 @@ import LeanCamCombi.Mathlib.Analysis.Convex.Independence
 import LeanCamCombi.Mathlib.Analysis.Convex.SimplicialComplex.Basic
 import LeanCamCombi.Mathlib.Combinatorics.Additive.VerySmallDoubling
 import LeanCamCombi.Mathlib.Combinatorics.Schnirelmann
+import LeanCamCombi.Mathlib.Combinatorics.SetFamily.Shatter
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Basic
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Density
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Finite
@@ -54,7 +55,9 @@ import LeanCamCombi.Mathlib.Data.List.DropRight
 import LeanCamCombi.Mathlib.Data.Multiset.Basic
 import LeanCamCombi.Mathlib.Data.Prod.Lex
 import LeanCamCombi.Mathlib.Data.Set.Basic
+import LeanCamCombi.Mathlib.Data.Set.Finite.Basic
 import LeanCamCombi.Mathlib.Data.Set.Image
+import LeanCamCombi.Mathlib.Data.Set.Lattice
 import LeanCamCombi.Mathlib.Data.Set.Pointwise.SMul
 import LeanCamCombi.Mathlib.GroupTheory.OrderOfElement
 import LeanCamCombi.Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
@@ -67,10 +70,13 @@ import LeanCamCombi.Mathlib.Order.RelIso.Group
 import LeanCamCombi.Mathlib.Probability.ProbabilityMassFunction.Constructions
 import LeanCamCombi.Mathlib.RingTheory.FinitePresentation
 import LeanCamCombi.Mathlib.RingTheory.Localization.Integral
+import LeanCamCombi.Mathlib.Topology.MetricSpace.MetricSeparated
 import LeanCamCombi.MetricBetween
 import LeanCamCombi.MinkowskiCaratheodory
 import LeanCamCombi.Multipartite
-import LeanCamCombi.PhD.VCDim.Basic
+import LeanCamCombi.PhD.VCDim.AddVCDim
+import LeanCamCombi.PhD.VCDim.HausslerPacking
+import LeanCamCombi.PhD.VCDim.HypercubeEdges
 import LeanCamCombi.PlainCombi.LittlewoodOfford
 import LeanCamCombi.PlainCombi.OrderShatter
 import LeanCamCombi.PlainCombi.VanDenBergKesten

LeanCamCombi/Mathlib/Combinatorics/SetFamily/Shatter.lean

@@ -0,0 +1,35 @@
+import Mathlib.Combinatorics.SetFamily.Shatter
+
+variable {α : Type*}
+
+section SemilatticeInf
+variable [SemilatticeInf α] {𝒜 ℬ : Set α} {A B : α}
+
+/-- A set family `𝒜` shatters a set `A` if all subsets of `A` can be obtained as the intersection
+of `A` with some element of the set family. We also say that `A` is *traced* by `𝒜`. -/
+def Shatters (𝒜 : Set α) (A : α) : Prop := ∀ ⦃B⦄, B ≤ A → ∃ C ∈ 𝒜, A ⊓ C = B
+
+lemma Shatters.mono (h : 𝒜 ⊆ ℬ) (h𝒜 : Shatters 𝒜 A) : Shatters ℬ A :=
+  fun _B hB ↦ let ⟨C, hC, hCB⟩ := h𝒜 hB; ⟨C, h hC, hCB⟩
+
+lemma Shatters.anti (h : A ≤ B) (hB : Shatters 𝒜 B) : Shatters 𝒜 A := fun C hC ↦ by
+  obtain ⟨D, hD, rfl⟩ := hB (hC.trans h); exact ⟨D, hD, inf_congr_right hC <| inf_le_of_left_le h⟩
+
+end SemilatticeInf
+
+section Set
+variable {d d₁ d₂ : ℕ} {𝒜 ℬ : Set (Set α)}
+
+open scoped Finset
+
+/-- A set family `𝒜` is `d`-NIP if it has VC dimension at most `d`, namely if all the sets it
+shatters have size at most `d`. -/
+def IsNIPWith (d : ℕ) (𝒜 : Set (Set α)) : Prop := ∀ ⦃A : Finset α⦄, Shatters 𝒜 A → #A ≤ d
+
+lemma IsNIPWith.anti (hℬ𝒜 : ℬ ⊆ 𝒜) (h𝒜 : IsNIPWith d 𝒜) : IsNIPWith d ℬ :=
+  fun _A hA ↦ h𝒜 <| hA.mono hℬ𝒜
+
+lemma IsNIPWith.mono (hd : d₁ ≤ d₂) (hd₁ : IsNIPWith d₁ 𝒜) : IsNIPWith d₂ 𝒜 :=
+  fun _A hA ↦ (hd₁ hA).trans hd
+
+end Set

LeanCamCombi/Mathlib/Data/Set/Basic.lean

@@ -6,4 +6,7 @@ variable {α : Type*} {s : Set α} {a : α}
 lemma sdiff_inter_right_comm (s t u : Set α) : s \ t ∩ u = (s ∩ u) \ t := by
   ext; simp [and_right_comm]
 
+lemma inter_sdiff_left_comm (s t u : Set α) : s ∩ (t \ u) = t ∩ (s \ u) := by
+  simp_rw [← inter_diff_assoc, inter_comm]
+
 end Set

LeanCamCombi/Mathlib/Data/Set/Finite/Basic.lean

@@ -0,0 +1,12 @@
+import Mathlib.Data.Set.Finite.Basic
+
+namespace Set
+variable {α : Type*} {s t u : Set α}
+
+open scoped symmDiff
+
+lemma Finite.symmDiff_congr (hst : (s ∆ t).Finite) : (s ∆ u).Finite ↔ (t ∆ u).Finite where
+  mp hsu := (hst.union hsu).subset (symmDiff_comm s t ▸ symmDiff_triangle ..)
+  mpr htu := (hst.union htu).subset (symmDiff_triangle ..)
+
+end Set

LeanCamCombi/Mathlib/Data/Set/Lattice.lean

@@ -0,0 +1,24 @@
+import Mathlib.Data.Set.Lattice
+
+section
+variable {α : Type*} [CompleteLattice α]
+
+lemma iInf_le_iSup {ι : Sort*} [Nonempty ι] {f : ι → α} : ⨅ i, f i ≤ ⨆ i, f i :=
+  (iInf_le _ (Classical.arbitrary _)).trans <| le_iSup _ (Classical.arbitrary _)
+
+lemma biInf_le_biSup {ι : Type*} {s : Set ι} (hs : s.Nonempty) {f : ι → α} :
+    ⨅ i ∈ s, f i ≤ ⨆ i ∈ s, f i :=
+  (biInf_le _ hs.choose_spec).trans <| le_biSup _ hs.choose_spec
+
+end
+
+namespace Set
+variable {α : Type*} {s : Set α} {a : α}
+
+lemma iInter_subset_iUnion {ι : Sort*} [Nonempty ι] {f : ι → Set α} : ⋂ i, f i ⊆ ⋃ i, f i :=
+  iInf_le_iSup
+
+lemma biInter_subset_biUnion {ι : Type*} {s : Set ι} (hs : s.Nonempty) {f : ι → Set α} :
+    ⋂ i ∈ s, f i ⊆ ⋃ i ∈ s, f i := biInf_le_biSup hs
+
+end Set

LeanCamCombi/Mathlib/Topology/MetricSpace/MetricSeparated.lean

@@ -0,0 +1,16 @@
+import Mathlib.Topology.MetricSpace.MetricSeparated
+
+/-!
+# TODO
+
+Rename `IsMetricSeparated` to `Metric.AreSeparated`
+-/
+
+open scoped ENNReal
+
+namespace Metric
+variable {X : Type*} [EMetricSpace X] {ε : ℝ≥0∞} {s t : Set X}
+
+def IsSeparated (ε : ℝ≥0∞) (s : Set X) : Prop := s.Pairwise (ε ≤ edist · ·)
+
+end Metric

LeanCamCombi/PhD/VCDim/HausslerPacking.lean

@@ -0,0 +1,38 @@
+/-
+Copyright (c) 2025 Yaël Dillies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies
+-/
+import Mathlib.Analysis.Normed.Lp.WithLp
+import Mathlib.Data.Complex.Exponential
+import LeanCamCombi.Mathlib.Topology.MetricSpace.MetricSeparated
+import LeanCamCombi.PhD.VCDim.HypercubeEdges
+
+/-!
+# 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
+-/
+
+open Fintype Metric Real
+open scoped Finset NNReal
+
+namespace SetFamily
+variable {α : Type*} [Fintype α] {𝓕 : Finset (Set α)} {k d : ℕ}
+
+/-- The **Haussler packing lemma** -/
+theorem haussler_packing (isNIPWith_𝓕 : IsNIPWith d 𝓕.toSet)
+    (isSeparated_𝓕 : IsSeparated (k / card α)
+      ((fun A : Set α ↦ (WithLp.equiv 1 _).symm A.indicator (1 : α → ℝ)) '' 𝓕))
+    (hk : k ≤ card α) : #𝓕 ≤ exp 1 * (d + 1) * (2 * exp 1 * (card α + 1) / (k + 2 * d + 2)) :=
+  sorry
+
+end SetFamily

LeanCamCombi/PhD/VCDim/HypercubeEdges.lean

@@ -0,0 +1,156 @@
+/-
+Copyright (c) 2025 Yaël Dillies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies
+-/
+import Mathlib.Algebra.BigOperators.Ring
+import Mathlib.Algebra.Order.BigOperators.Group.Finset
+import Mathlib.Data.Set.Card
+import Mathlib.Data.Set.Finite.Lattice
+import Mathlib.Order.Partition.Finpartition
+import LeanCamCombi.Mathlib.Combinatorics.SetFamily.Shatter
+import LeanCamCombi.Mathlib.Data.Set.Finite.Basic
+import LeanCamCombi.Mathlib.Data.Set.Lattice
+
+/-!
+# A small VC dimension family has few edges in the L¹ metric
+
+This file proves that set families over a finite type that have small VC dimension have a number
+of pairs `(A, B)` with `#(A ∆ B) = 1` linear in their size.
+
+## 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
+-/
+
+open Finset
+open scoped symmDiff
+
+namespace SetFamily
+variable {α : Type*} {𝓕 𝓒 : Finset (Set α)} {A B : Set α} {d : ℕ}
+
+/-- The edges of the subgraph of the hypercube `Set α` induced by a finite set of vertices
+`𝓕 : Finset (Set α)`. -/
+noncomputable def hypercubeEdgeFinset (𝓕 : Finset (Set α)) : Finset (Set α × Set α) :=
+  {AB ∈ 𝓕 ×ˢ 𝓕 | (AB.1 ∆ AB.2).ncard = 1}
+
+@[simp] lemma prodMk_mem_hypercubeEdgeFinset :
+    (A, B) ∈ hypercubeEdgeFinset 𝓕 ↔ A ∈ 𝓕 ∧ B ∈ 𝓕 ∧ (A ∆ B).ncard = 1 := by
+  simp [hypercubeEdgeFinset, and_assoc]
+
+open scoped Classical in
+@[simp]
+private lemma filter_finite_symmDiff_inj (hB : B ∈ 𝓕) :
+    {C ∈ 𝓕 | (A ∆ C).Finite} = {C ∈ 𝓕 | (B ∆ C).Finite} ↔ (A ∆ B).Finite where
+  mp hAB := by
+    have : B ∈ {C ∈ 𝓕 | (A ∆ C).Finite} := hAB ▸ mem_filter.2 ⟨hB, by simp⟩
+    exact (mem_filter.1 this).2
+  mpr hAB := by ext D; simp [hAB.symmDiff_congr]
+
+open scoped Classical in
+/-- Partition a set family into its components of finite symmetric difference. -/
+noncomputable def finiteSymmDiffFinpartition (𝓕 : Finset (Set α)) : Finpartition 𝓕 where
+  parts := 𝓕.image fun A ↦ {B ∈ 𝓕 | (A ∆ B).Finite}
+  supIndep := by
+    simp +contextual only [supIndep_iff_pairwiseDisjoint, Set.PairwiseDisjoint, Set.Pairwise,
+      coe_image, Set.mem_image, mem_coe, ne_eq, Function.onFun, id, disjoint_left,
+      forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, mem_filter, not_and, forall_const,
+      filter_finite_symmDiff_inj]
+    refine fun A hA B hB hAB C hC hAC hBC ↦ hAB ?_
+    exact (hAC.union <| symmDiff_comm B C ▸ hBC).subset <| symmDiff_triangle ..
+  sup_parts := by
+    simp only [sup_image, le_antisymm_iff, Finset.sup_le_iff, le_eq_subset,
+      filter_subset, implies_true, true_and, Function.id_comp]
+    exact fun A hA ↦ mem_sup.2 ⟨A, hA, mem_filter.2 ⟨hA, by simp⟩⟩
+  not_bot_mem := by
+    simp only [bot_eq_empty, mem_image, filter_eq_empty_iff, not_exists, not_and, not_forall,
+      Classical.not_imp, Decidable.not_not]
+    exact fun A hA ↦ ⟨A, hA, by simp⟩
+
+open scoped Classical in
+lemma finite_symmDiff_of_mem_finiteSymmDiffFinpartition
+    (h𝓒 : 𝓒 ∈ (finiteSymmDiffFinpartition 𝓕).parts) (hA : A ∈ 𝓒) (hB : B ∈ 𝓒) :
+    (A ∆ B).Finite := by
+  simp only [finiteSymmDiffFinpartition, mem_image] at h𝓒
+  obtain ⟨C, hC, rfl⟩ := h𝓒
+  rw [mem_filter] at hA hB
+  exact ((symmDiff_comm A C ▸ hA.2).union hB.2).subset <| symmDiff_triangle ..
+
+open scoped Classical in
+lemma finite_iUnion_sdiff_iInter_of_mem_finiteSymmDiffFinpartition
+    (h𝓒 : 𝓒 ∈ (finiteSymmDiffFinpartition 𝓕).parts) : ((⋃ A ∈ 𝓒, A) \ ⋂ A ∈ 𝓒, A).Finite := by
+  simp_rw [Set.iUnion_diff, Set.diff_iInter]
+  exact .biUnion 𝓒.finite_toSet fun A hA ↦ .biUnion 𝓒.finite_toSet fun B hB ↦
+    (finite_symmDiff_of_mem_finiteSymmDiffFinpartition h𝓒 hA hB).subset le_sup_left
+
+open scoped Classical in
+@[simp]
+lemma sup_finiteSymmDiffFinpartition_hypercubeEdgeFinset (𝓕 : Finset (Set α)) :
+    (finiteSymmDiffFinpartition 𝓕).parts.sup hypercubeEdgeFinset = hypercubeEdgeFinset 𝓕 := by
+  ext ⟨A, B⟩
+  simp only [finiteSymmDiffFinpartition, sup_image, mem_sup, Function.comp_apply,
+    prodMk_mem_hypercubeEdgeFinset, mem_filter, and_assoc, and_left_comm, exists_and_left,
+    and_congr_right_iff, Set.ncard_eq_one]
+  refine fun hA hB ↦ ⟨?_, ?_⟩
+  · rintro ⟨C, hC, hCA, hCB, hAB⟩
+    exact hAB
+  · rintro ⟨a, ha⟩
+    exact ⟨A, by simp [*]⟩
+
+open scoped Classical Set.Notation in
+/-- Restrict a component of finite symmetric difference to a set family over a finite type. -/
+noncomputable def restrictFiniteSymmDiffComponent (𝓒 : Finset (Set α)) :
+    Finset (Set ↥((⋃ A ∈ 𝓒, A) \ ⋂ A ∈ 𝓒, A)) :=
+  𝓒.image fun A ↦ _ ↓∩ A ∆ ⋂ B ∈ 𝓒, B
+
+@[simp] lemma card_restrictFiniteSymmDiffComponent (𝓒 : Finset (Set α)) :
+    #(restrictFiniteSymmDiffComponent 𝓒) = #𝓒 := by
+  classical
+  refine card_image_of_injOn fun A hA B hB hAB ↦ ?_
+  replace hAB := congr(Subtype.val '' $hAB)
+  have : (⋃ A ∈ 𝓒, A) ∆ ⋂ B ∈ 𝓒, B = ((⋃ A ∈ 𝓒, A) \ ⋂ B ∈ 𝓒, B) :=
+    symmDiff_of_ge <| Set.biInter_subset_biUnion ⟨A, hA⟩
+  stop
+  simp_rw [Set.image_preimage_eq_inter_range, Subtype.range_val, ← this, ← Set.inter_symmDiff_distrib_left, Set.inter_sdiff_left_comm _ (⋃ _, _)] at hAB
+
+
+protected lemma _root_.IsNIPWith.restrictFiniteSymmDiffComponent (h𝓒 : IsNIPWith d 𝓒.toSet) :
+    IsNIPWith d (restrictFiniteSymmDiffComponent 𝓒).toSet := sorry
+
+private lemma _root_.IsNIPWith.card_hypercubeEdgeFinset_le_of_finite [Finite α]
+    (h𝓕 : IsNIPWith d 𝓕.toSet) : #(hypercubeEdgeFinset 𝓕) ≤ d * #𝓕 := by
+  sorry
+
+lemma IsNIPWith.card_hypercubeEdgeFinset_le (h𝓕 : IsNIPWith d 𝓕.toSet) :
+    #(hypercubeEdgeFinset 𝓕) ≤ d * #𝓕 := by
+  classical
+  calc
+    #(hypercubeEdgeFinset 𝓕)
+    _ = ∑ 𝓒 ∈ (finiteSymmDiffFinpartition 𝓕).parts, #(hypercubeEdgeFinset 𝓒) := by
+      rw [← sup_finiteSymmDiffFinpartition_hypercubeEdgeFinset, sup_eq_biUnion, card_biUnion]
+      simp +contextual only [finiteSymmDiffFinpartition, mem_image, ne_eq, hypercubeEdgeFinset,
+        disjoint_left, mem_filter, mem_product, and_true, not_and, and_imp,
+        forall_exists_index, Prod.forall, forall_apply_eq_imp_iff₂, forall_const,
+        filter_finite_symmDiff_inj]
+      refine fun A hA B hB hAB C D hC hAC hD hAD hCD hBC hBD ↦ hAB ?_
+      exact (hAC.union <| symmDiff_comm B C ▸ hBC).subset <| symmDiff_triangle ..
+    _ ≤ ∑ 𝓒 ∈ (finiteSymmDiffFinpartition 𝓕).parts, d * #𝓒 := by
+      gcongr with 𝓒 h𝓒
+      have : Finite ↥((⋃ A ∈ 𝓒, A) \ ⋂ A ∈ 𝓒, A) :=
+        finite_iUnion_sdiff_iInter_of_mem_finiteSymmDiffFinpartition h𝓒
+      calc
+        #(hypercubeEdgeFinset 𝓒)
+        _ = #(hypercubeEdgeFinset (restrictFiniteSymmDiffComponent 𝓒)) := sorry
+        _ ≤ d * #(restrictFiniteSymmDiffComponent 𝓒) := by
+          refine (h𝓕.anti ?_).restrictFiniteSymmDiffComponent.card_hypercubeEdgeFinset_le_of_finite
+          gcongr
+          exact mod_cast (finiteSymmDiffFinpartition 𝓕).le h𝓒
+        _ = d * #𝓒 := by rw [card_restrictFiniteSymmDiffComponent]
+    _  = d * #𝓕 := by
+      rw [← mul_sum, ← card_biUnion, ← sup_eq_biUnion]
+      erw [(finiteSymmDiffFinpartition 𝓕).sup_parts]
+      exact supIndep_iff_pairwiseDisjoint.1 (finiteSymmDiffFinpartition 𝓕).supIndep
+
+end SetFamily