From f62db726a9ccc6eff8f1e9541319c8d8c675f63a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Wed, 25 Sep 2024 07:19:32 +0000
Subject: [PATCH] Define the multiplicative VC dimension

---
 .../Combinatorics/SetFamily/Shatter.lean      | 47 +---------------
 LeanCamCombi/OrderShatter.lean                | 55 +++++++++++++++++++
 LeanCamCombi/PhD/VCDim/Basic.lean             | 23 ++++++++
 3 files changed, 80 insertions(+), 45 deletions(-)
 create mode 100644 LeanCamCombi/OrderShatter.lean
 create mode 100644 LeanCamCombi/PhD/VCDim/Basic.lean

diff --git a/LeanCamCombi/Mathlib/Combinatorics/SetFamily/Shatter.lean b/LeanCamCombi/Mathlib/Combinatorics/SetFamily/Shatter.lean
index c86658d996..5a0b85ad8a 100644
--- a/LeanCamCombi/Mathlib/Combinatorics/SetFamily/Shatter.lean
+++ b/LeanCamCombi/Mathlib/Combinatorics/SetFamily/Shatter.lean
@@ -1,55 +1,12 @@
-/-
-Copyright (c) 2022 Yaël Dillies. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Yaël Dillies
--/
 import Mathlib.Combinatorics.SetFamily.Shatter
-import Mathlib.Data.Finset.Sort
-
-/-!
-# Shattering families
-
-This file defines the shattering property and VC-dimension of set families.
-
-## Main declarations
-
-* `Finset.StronglyShatters`:
-* `Finset.OrderShatters`:
-
-## TODO
-
-* Order-shattering
-* Strong shattering
--/
 
 open scoped BigOperators FinsetFamily
 
 namespace Finset
 variable {α : Type*} [DecidableEq α] {𝒜 ℬ : Finset (Finset α)} {s t : Finset α} {a : α} {n : ℕ}
 
-/-! ### Strong shattering -/
-
-def StronglyShatters (𝒜 : Finset (Finset α)) (s : Finset α) : Prop :=
-  ∃ t, ∀ ⦃u⦄, u ⊆ s → ∃ v ∈ 𝒜, s ∩ v = u ∧ v \ s = t
-
-/-! ### Order shattering -/
-
-section order
-variable [LinearOrder α]
-
-def OrderShatters : Finset (Finset α) → List α → Prop
-  | 𝒜, [] => 𝒜.Nonempty
-  | 𝒜, a :: l => (𝒜.nonMemberSubfamily a).OrderShatters l ∧ (𝒜.memberSubfamily a).OrderShatters l
-      ∧ ∀ ⦃s : Finset α⦄, s ∈ 𝒜.nonMemberSubfamily a → ∀ ⦃t⦄, t ∈ 𝒜.memberSubfamily a →
-        s.filter (a < ·) = t.filter (a < ·)
-
-instance : DecidablePred 𝒜.OrderShatters
-  | [] => decidableNonempty
-  | a :: l => by unfold OrderShatters; sorry
-
-def orderShatterser (𝒜 : Finset (Finset α)) : Finset (Finset α) :=
-  (𝒜.biUnion powerset).filter fun s ↦ 𝒜.OrderShatters $ s.sort (· ≤ ·)
+attribute [gcongr] shatterer_mono
 
-end order
+@[gcongr] lemma vcDim_mono (h𝒜ℬ : 𝒜 ⊆ ℬ) : 𝒜.vcDim ≤ ℬ.vcDim := by unfold vcDim; gcongr
 
 end Finset
diff --git a/LeanCamCombi/OrderShatter.lean b/LeanCamCombi/OrderShatter.lean
new file mode 100644
index 0000000000..c86658d996
--- /dev/null
+++ b/LeanCamCombi/OrderShatter.lean
@@ -0,0 +1,55 @@
+/-
+Copyright (c) 2022 Yaël Dillies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies
+-/
+import Mathlib.Combinatorics.SetFamily.Shatter
+import Mathlib.Data.Finset.Sort
+
+/-!
+# Shattering families
+
+This file defines the shattering property and VC-dimension of set families.
+
+## Main declarations
+
+* `Finset.StronglyShatters`:
+* `Finset.OrderShatters`:
+
+## TODO
+
+* Order-shattering
+* Strong shattering
+-/
+
+open scoped BigOperators FinsetFamily
+
+namespace Finset
+variable {α : Type*} [DecidableEq α] {𝒜 ℬ : Finset (Finset α)} {s t : Finset α} {a : α} {n : ℕ}
+
+/-! ### Strong shattering -/
+
+def StronglyShatters (𝒜 : Finset (Finset α)) (s : Finset α) : Prop :=
+  ∃ t, ∀ ⦃u⦄, u ⊆ s → ∃ v ∈ 𝒜, s ∩ v = u ∧ v \ s = t
+
+/-! ### Order shattering -/
+
+section order
+variable [LinearOrder α]
+
+def OrderShatters : Finset (Finset α) → List α → Prop
+  | 𝒜, [] => 𝒜.Nonempty
+  | 𝒜, a :: l => (𝒜.nonMemberSubfamily a).OrderShatters l ∧ (𝒜.memberSubfamily a).OrderShatters l
+      ∧ ∀ ⦃s : Finset α⦄, s ∈ 𝒜.nonMemberSubfamily a → ∀ ⦃t⦄, t ∈ 𝒜.memberSubfamily a →
+        s.filter (a < ·) = t.filter (a < ·)
+
+instance : DecidablePred 𝒜.OrderShatters
+  | [] => decidableNonempty
+  | a :: l => by unfold OrderShatters; sorry
+
+def orderShatterser (𝒜 : Finset (Finset α)) : Finset (Finset α) :=
+  (𝒜.biUnion powerset).filter fun s ↦ 𝒜.OrderShatters $ s.sort (· ≤ ·)
+
+end order
+
+end Finset
diff --git a/LeanCamCombi/PhD/VCDim/Basic.lean b/LeanCamCombi/PhD/VCDim/Basic.lean
new file mode 100644
index 0000000000..7cfd562733
--- /dev/null
+++ b/LeanCamCombi/PhD/VCDim/Basic.lean
@@ -0,0 +1,23 @@
+import LeanCamCombi.Mathlib.Combinatorics.SetFamily.Shatter
+import Mathlib.Algebra.Group.Pointwise.Finset.Basic
+
+open scoped Pointwise
+
+namespace Finset
+variable {G : Type*} [Group G] [DecidableEq G] {A B B₁ B₂ : Finset G}
+
+@[to_additive] def mulVCDim (A B : Finset G) : ℕ := ((B / A).image (· • A ∩ B)).vcDim
+
+@[to_additive (attr := gcongr)]
+lemma mulVCDim_mono (hB : B₁ ⊆ B₂) : mulVCDim A B₁ ≤ mulVCDim A B₂ := by
+  refine sup_mono ?_
+  simp only [subset_iff, mem_shatterer, Shatters, mem_image, exists_exists_and_eq_and]
+  rintro C hC D hD
+  have hCB : C ⊆ B₁ := by
+    obtain ⟨x, -, h⟩ := hC fun x hx ↦ hx
+    exact (inter_eq_left.1 h).trans inter_subset_right
+  obtain ⟨x, hx, rfl⟩ := hC hD
+  refine ⟨x, div_subset_div_right hB hx, ?_⟩
+  rw [inter_left_comm, inter_eq_left.2 <| hCB.trans hB, inter_left_comm, inter_eq_left.2 hCB]
+
+end Finset