PlainCombi: Symmetric Chain Decomposition

LeanCamCombi.lean

@@ -14,7 +14,11 @@ import LeanCamCombi.Mathlib.Combinatorics.SetFamily.LYM
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Copy
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Density
 import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Subgraph
+import LeanCamCombi.Mathlib.Data.Finset.Image
+import LeanCamCombi.Mathlib.Data.Set.Function
 import LeanCamCombi.Mathlib.Probability.ProbabilityMassFunction.Constructions
+import LeanCamCombi.PlainCombi.Chap1.Sec1.SCD
+import LeanCamCombi.PlainCombi.Chap1.Sec1.SDSS
 import LeanCamCombi.PlainCombi.KatonaCircle
 import LeanCamCombi.PlainCombi.LittlewoodOfford
 import LeanCamCombi.PlainCombi.OrderShatter

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

LeanCamCombi/PlainCombi/Chap1/Sec1/SCD.lean

@@ -0,0 +1,103 @@
+/-
+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.Order.Partition.Finpartition
+import LeanCamCombi.Mathlib.Data.Finset.Image
+
+/-!
+# Symmetric Chain Decompositions
+
+This file shows that if `α` is finite then `Finset α` has a decomposition into symmetric chains,
+namely chains of the form `{Cᵢ, ..., Cₙ₋ᵢ}` where `card α = n` and `|C_j| = j`.
+-/
+
+open Finset
+
+namespace Finpartition
+variable {α : Type*} [DecidableEq α] {𝒜 : Finset (Finset α)} {𝒞 𝒟 : Finset (Finset α)}
+  {C s : Finset α} {a : α}
+
+def extendExchange (a : α) (𝒞 : Finset (Finset α)) (C : Finset α) : Finset (Finset (Finset α)) :=
+  if 𝒞.Nontrivial
+  then {(𝒞 \ {C}).image (insert a), 𝒞 ∪ {insert a C}}
+  else {𝒞 ∪ {insert a C}}
+
+lemma eq_or_eq_of_mem_extendExchange :
+    𝒟 ∈ extendExchange a 𝒞 C → 𝒟 = (𝒞 \ {C}).image (insert a) ∨ 𝒟 = 𝒞 ∪ {insert a C} := by
+  unfold extendExchange; split_ifs with h𝒞 <;> simp (config := { contextual := true })
+
+@[simp] lemma not_empty_mem_extendExchange : ∅ ∉ extendExchange a 𝒞 C := by
+  unfold extendExchange
+  split_ifs with h𝒞
+  · simp [eq_comm (a := ∅), ← nonempty_iff_ne_empty, h𝒞.nonempty.ne_empty, h𝒞.ne_singleton]
+  · simp [eq_comm (a := ∅), ← nonempty_iff_ne_empty]
+
+@[simp] lemma sup_extendExchange (hC : C ∈ 𝒞) :
+    (extendExchange a 𝒞 C).sup id = 𝒞 ∪ 𝒞.image (insert a) := by
+  unfold extendExchange
+  split_ifs with h𝒞
+  · simp only [sup_insert, id_eq, sup_singleton, sup_eq_union, union_left_comm]
+    rw [image_sdiff_of_injOn, image_singleton, sdiff_union_of_subset]
+    · simpa using mem_image_of_mem _ hC
+    · sorry
+    · simpa
+  · obtain rfl := (eq_singleton_or_nontrivial hC).resolve_right h𝒞
+    simp
+
+def extendPowersetExchange (P : Finpartition s.powerset) (f : ∀ 𝒞 ∈ P.parts, 𝒞) (a : α)
+    (ha : a ∉ s) : Finpartition (s.cons a ha).powerset where
+
+  -- ofErase
+  --   (P.parts.attach.biUnion fun ⟨𝒞, h𝒞⟩ ↦ extendExchange a 𝒞 (f 𝒞 h𝒞).1)
+  --   (by
+  --     sorry
+  --     )
+  --   (by
+  --     simp
+  --     )
+
+  parts := P.parts.attach.biUnion fun ⟨𝒞, h𝒞⟩ ↦ extendExchange a 𝒞 (f 𝒞 h𝒞).1
+  supIndep := by
+    rw [Finset.supIndep_iff_pairwiseDisjoint]
+    simp only [Set.PairwiseDisjoint, Set.Pairwise, Finset.coe_biUnion, Finset.mem_coe,
+      Finset.mem_attach, Set.iUnion_true, Set.mem_iUnion, Subtype.exists, ne_eq, Function.onFun,
+      id_eq, forall_exists_index, not_imp_comm]
+    rintro x 𝒞 h𝒞 hx y 𝒟 h𝒟 hy hxy
+    obtain rfl | rfl := eq_or_eq_of_mem_extendExchange hx <;>
+      obtain rfl | rfl := eq_or_eq_of_mem_extendExchange hy
+    · rw [disjoint_image'] at hxy
+      · obtain rfl := P.disjoint.elim h𝒞 h𝒟 fun h ↦ hxy <| h.mono sdiff_le sdiff_le
+        rfl
+      · sorry
+    · sorry
+    · sorry
+    · simp_rw [disjoint_union_left, disjoint_union_right, and_assoc] at hxy
+      obtain rfl := P.disjoint.elim h𝒞 h𝒟 fun h ↦ hxy <| ⟨h, sorry, sorry, sorry⟩
+      rfl
+  sup_parts := by
+    ext C
+    simp only [sup_biUnion, coe_mem, sup_extendExchange, mem_sup, mem_attach, mem_union, mem_image,
+      true_and, Subtype.exists, exists_prop, cons_eq_insert, mem_powerset]
+    constructor
+    · rintro ⟨𝒞, h𝒞, hC | ⟨C, hC, rfl⟩⟩
+      · exact Subset.trans (mem_powerset.1 <| P.le h𝒞 hC) (subset_insert ..)
+      · exact insert_subset_insert _ (mem_powerset.1 <| P.le h𝒞 hC)
+    by_cases ha : a ∈ C
+    · rw [subset_insert_iff]
+      rintro hC
+      obtain ⟨𝒞, h𝒞, hC⟩ := P.exists_mem <| mem_powerset.2 hC
+      exact ⟨𝒞, h𝒞, .inr ⟨_, hC, insert_erase ha⟩⟩
+    · rw [subset_insert_iff_of_not_mem ha]
+      rintro hC
+      obtain ⟨𝒞, h𝒞, hC⟩ := P.exists_mem <| mem_powerset.2 hC
+      exact ⟨𝒞, h𝒞, .inl hC⟩
+  not_bot_mem := by simp
+
+/-! ### Profile of a partition -/
+
+/-- The profile of  -/
+def profile (P : Finpartition s) : Multiset ℕ := P.parts.1.map card
+
+end Finpartition

LeanCamCombi/PlainCombi/Chap1/Sec1/SDSS.lean

@@ -0,0 +1,57 @@
+/-
+Copyright (c) 2022 Yaël Dillies. All rights reserved.
+Released under Apache 2.0 license as described ∈ the file LICENSE.
+Authors: Yaël Dillies
+-/
+import Mathlib.Analysis.NormedSpace.HahnBanach.Extension
+import Mathlib.Combinatorics.Enumerative.DoubleCounting
+import Mathlib.Order.Partition.Finpartition
+import LeanCamCombi.PlainCombi.Chap1.Sec1.SCD
+
+/-!
+# Symmetric Decompositions into Sparse Sets
+
+The Littlewood-Offord problem
+-/
+
+open scoped BigOperators
+
+namespace Finset
+variable {α E : Type*} {𝒜 : Finset (Finset α)}
+  {s : Finset α} {f : α → E} {r : ℝ}
+
+def profile (𝒜 : Finset (Finset α)) : Multiset ℕ := sorry
+
+-- def subpartition (f : ):
+
+variable [NormedAddCommGroup E] [NormedSpace ℝ E]
+
+lemma exists_littlewood_offord_partition [DecidableEq α] (hr : 0 < r) (hf : ∀ i ∈ s, r ≤ ‖f i‖) :
+    ∃ P : Finpartition s.powerset,
+      #P.parts = (#s).choose (s.card / 2) ∧
+        (∀ 𝒜 ∈ P.parts, ∀ t ∈ 𝒜, t ⊆ s) ∧
+          ∀ 𝒜 ∈ P.parts,
+            (𝒜 : Set (Finset α)).Pairwise fun u v ↦ r ≤ dist (∑ i ∈ u, f i) (∑ i ∈ v, f i) := by
+  classical
+  induction' s using Finset.induction with i s hi ih
+  · exact ⟨Finpartition.indiscrete <| singleton_ne_empty _, by simp⟩
+  obtain ⟨P, hP, hs, hPr⟩ := ih fun j hj ↦ hf _ <| mem_insert_of_mem hj
+  clear ih
+  obtain ⟨g, hg, hgf⟩ :=
+    exists_dual_vector ℝ (f i) (norm_pos_iff.1 <| hr.trans_le <| hf _ <| mem_insert_self _ _)
+  choose! t ht using fun 𝒜 (h𝒜 : 𝒜 ∈ P.parts) ↦
+    Finset.exists_max_image _ (fun t ↦ g (∑ i ∈ t, f i)) (P.nonempty_of_mem_parts h𝒜)
+  sorry
+
+/-- **Kleitman's lemma** -/
+lemma card_le_of_forall_dist_sum_le (hr : 0 < r) (h𝒜 : ∀ t ∈ 𝒜, t ⊆ s) (hf : ∀ i ∈ s, r ≤ ‖f i‖)
+    (h𝒜r : ∀ u, u ∈ 𝒜 → ∀ v, v ∈ 𝒜 → dist (∑ i ∈ u, f i) (∑ i ∈ v, f i) < r) :
+    #𝒜 ≤ (#s).choose (#s / 2) := by
+  classical
+  obtain ⟨P, hP, _hs, hr⟩ := exists_littlewood_offord_partition hr hf
+  rw [← hP]
+  refine card_le_card_of_forall_subsingleton (· ∈ ·) (fun t ht ↦ ?_) fun ℬ hℬ t ht u hu ↦
+    (hr _ hℬ).eq ht.2 hu.2 (h𝒜r _ ht.1 _ hu.1).not_le
+  simpa only [exists_prop] using P.exists_mem (mem_powerset.2 <| h𝒜 _ ht)
+
+end Finset

LeanCamCombi/PlainCombi/LittlewoodOfford.lean

@@ -1,26 +1,33 @@
 /-
 Copyright (c) 2022 Yaël Dillies. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
+Released under Apache 2.0 license as described ∈ the file LICENSE.
 Authors: Yaël Dillies
 -/
 import Mathlib.Analysis.NormedSpace.HahnBanach.Extension
 import Mathlib.Combinatorics.Enumerative.DoubleCounting
 import Mathlib.Order.Partition.Finpartition
+import LeanCamCombi.PlainCombi.Chap1.Sec1.SCD
 
 /-!
-# The Littlewood-Offord problem
+# Symmetric Decompositions into Sparse Sets
+
+The Littlewood-Offord problem
 -/
 
 open scoped BigOperators
 
 namespace Finset
-variable {ι E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {𝒜 : Finset (Finset ι)}
-  {s : Finset ι} {f : ι → E} {r : ℝ}
+variable {α E : Type*} {𝒜 : Finset (Finset α)}
+  {s : Finset α} {f : α → E} {r : ℝ}
+
+-- def subpartition (f : ):
+
+variable [NormedAddCommGroup E] [NormedSpace ℝ E]
 
-lemma exists_littlewood_offord_partition [DecidableEq ι] (hr : 0 < r) (hf : ∀ i ∈ s, r ≤ ‖f i‖) :
-    ∃ P : Finpartition s.powerset,
-      #P.parts = (#s).choose (#s / 2) ∧ (∀ 𝒜 ∈ P.parts, ∀ t ∈ 𝒜, t ⊆ s) ∧ ∀ 𝒜 ∈ P.parts,
-        (𝒜 : Set (Finset ι)).Pairwise fun u v ↦ r ≤ dist (∑ i ∈ u, f i) (∑ i ∈ v, f i) := by
+lemma exists_littlewood_offord_partition [DecidableEq α] (hr : 0 < r) (hf : ∀ i ∈ s, r ≤ ‖f i‖) :
+    ∃ P : Finpartition s.powerset, #P.parts = (#s).choose (#s / 2) ∧
+      (∀ 𝒜 ∈ P.parts, ∀ t ∈ 𝒜, t ⊆ s) ∧
+        ∀ 𝒜 ∈ P.parts, 𝒜.toSet.Pairwise fun u v ↦ r ≤ dist (∑ i ∈ u, f i) (∑ i ∈ v, f i) := by
   classical
   induction' s using Finset.induction with i s hi ih
   · exact ⟨Finpartition.indiscrete <| singleton_ne_empty _, by simp⟩