PlainCombi: Symmetric Chain Decomposition

LeanCamCombi.lean

@@ -30,12 +30,13 @@ import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Density
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Finite
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Maps
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Subgraph
+import LeanCamCombi.Mathlib.Data.Finset.Image
 import LeanCamCombi.Mathlib.Data.List.DropRight
 import LeanCamCombi.Mathlib.Data.Multiset.Basic
+import LeanCamCombi.Mathlib.Data.Set.Function
 import LeanCamCombi.Mathlib.Data.Set.Pointwise.SMul
 import LeanCamCombi.Mathlib.GroupTheory.OrderOfElement
 import LeanCamCombi.Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
-import LeanCamCombi.Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
 import LeanCamCombi.Mathlib.Order.Flag
 import LeanCamCombi.Mathlib.Order.Partition.Finpartition
 import LeanCamCombi.Mathlib.Order.RelIso.Group
@@ -45,9 +46,10 @@ import LeanCamCombi.MetricBetween
 import LeanCamCombi.MinkowskiCaratheodory
 import LeanCamCombi.Multipartite
 import LeanCamCombi.PhD.VCDim.AddVCDim
-import LeanCamCombi.PhD.VCDim.CondVar
 import LeanCamCombi.PhD.VCDim.HausslerPacking
 import LeanCamCombi.PhD.VCDim.HypercubeEdges
+import LeanCamCombi.PlainCombi.Chap1.Sec1.SCD
+import LeanCamCombi.PlainCombi.Chap1.Sec1.SDSS
 import LeanCamCombi.PlainCombi.LittlewoodOfford
 import LeanCamCombi.PlainCombi.OrderShatter
 import LeanCamCombi.PlainCombi.VanDenBergKesten

LeanCamCombi/GrowthInGroups/Lecture2.lean

@@ -33,10 +33,10 @@ lemma lemma_2_3_1 (hA : #(A ^ 2) ≤ K * #A) : #(A * A⁻¹) ≤ K ^ 2 * #A := b
 
 lemma lemma_2_4_1 (hm : 3 ≤ m) (hA : #(A ^ 3) ≤ K * #A) (ε : Fin m → ℤ) (hε : ∀ i, |ε i| = 1) :
     #((finRange m).map fun i ↦ A ^ ε i).prod ≤ K ^ (3 * (m - 2)) * #A :=
-  small_alternating_pow_of_small_tripling' hm hA ε hε
+  small_alternating_pow_of_small_tripling hm hA ε hε
 
 lemma lemma_2_4_2 (hm : 3 ≤ m) (hA : #(A ^ 3) ≤ K * #A) (hAsymm : A⁻¹ = A) :
-    #(A ^ m) ≤ K ^ (m - 2) * #A := small_pow_of_small_tripling' hm hA hAsymm
+    #(A ^ m) ≤ K ^ (m - 2) * #A := small_pow_of_small_tripling hm hA hAsymm
 
 def def_2_5 (S : Set G) (K : ℝ) : Prop := IsApproximateSubgroup K S
 

LeanCamCombi/Kneser/Kneser.lean

@@ -357,11 +357,11 @@ theorem mul_kneser :
       subset_mul_left _ $ one_mem_mulStab.2 $ hst.mul $ hs.mono subset_union_left) _).trans $
         ih (s ∩ t) (s ∪ t) ?_⟩
     exact add_lt_add_of_le_of_lt (card_le_card inter_mul_union_subset) (card_lt_card hsts)
-  let C := argminOn (fun C : Finset α => #C.mulStab) IsWellFounded.wf _ convergent_nonempty
+  let C := argminOn (fun C : Finset α => #C.mulStab) _ convergent_nonempty
   set H := C.mulStab with hH
-  obtain ⟨hCst, hCcard⟩ : C ∈ convergent := argminOn_mem _ _ _ _
-  have hCmin : ∀ D : Finset α, D.mulStab ⊂ H → ¬D ∈ convergent := fun D hDH hD =>
-    (card_lt_card hDH).not_le $ argminOn_le (fun D : Finset α => #D.mulStab) _ _ hD
+  obtain ⟨hCst, hCcard⟩ : C ∈ convergent := argminOn_mem _ _ _
+  have hCmin (D : Finset α) (hDH : D.mulStab ⊂ H) : D ∉ convergent := fun hD ↦
+    (card_lt_card hDH).not_le $ argminOn_le (fun D : Finset α => #D.mulStab) _ hD
   clear_value C
   clear convergent_nonempty
   obtain rfl | hC := C.eq_empty_or_nonempty

LeanCamCombi/Mathlib/Data/Finset/Image.lean

@@ -0,0 +1,10 @@
+import Mathlib.Data.Finset.Image
+import LeanCamCombi.Mathlib.Data.Set.Function
+
+namespace Finset
+variable {α β : Type*} [DecidableEq β] {s t : Finset α} {f : α → β}
+
+lemma disjoint_image' (hf : Set.InjOn f (s ∪ t)) :
+    Disjoint (image f s) (image f t) ↔ Disjoint s t := mod_cast Set.disjoint_image' hf
+
+end Finset

LeanCamCombi/Mathlib/Data/Set/Function.lean

@@ -0,0 +1,11 @@
+import Mathlib.Data.Set.Function
+
+namespace Set
+variable {α β : Type*} {s t : Set α} {f : α → β}
+
+lemma disjoint_image' (hf : (s ∪ t).InjOn f) : Disjoint (f '' s) (f '' t) ↔ Disjoint s t where
+  mp := .of_image
+  mpr hst := disjoint_image_image fun _a ha _b hb ↦
+    hf.ne (.inl ha) (.inr hb) fun H ↦ Set.disjoint_left.1 hst ha (H ▸ hb)
+
+end Set