Skip to content

Commit d439774

Browse files
YaelDilliesYaelDillies
committed
Start on SCD
1 parent 5915513 commit d439774

File tree

11 files changed

+247
-11
lines changed

11 files changed

+247
-11
lines changed

‎LeanCamCombi.lean‎

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,7 @@
11
import LeanCamCombi.Archive.CauchyDavenportFromKneser
22
import LeanCamCombi.BernoulliSeq
3+
import LeanCamCombi.Combinatorics.Chap1.Sec1.SCD
4+
import LeanCamCombi.Combinatorics.Chap1.Sec1.SDSS
35
import LeanCamCombi.ConvexityRefactor.Defs
46
import LeanCamCombi.ConvexityRefactor.StdSimplex
57
import LeanCamCombi.Corners.CombiDegen
@@ -32,7 +34,6 @@ import LeanCamCombi.Incidence
3234
import LeanCamCombi.Kneser.Kneser
3335
import LeanCamCombi.Kneser.KneserRuzsa
3436
import LeanCamCombi.Kneser.MulStab
35-
import LeanCamCombi.LittlewoodOfford
3637
import LeanCamCombi.Mathlib.Algebra.Group.Pointwise.Finset.Basic
3738
import LeanCamCombi.Mathlib.Algebra.Group.Pointwise.Set.Basic
3839
import LeanCamCombi.Mathlib.Algebra.Group.Pointwise.Set.BigOperators
@@ -57,15 +58,21 @@ import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Density
5758
import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Maps
5859
import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Multipartite
5960
import LeanCamCombi.Mathlib.Combinatorics.SimpleGraph.Subgraph
61+
import LeanCamCombi.Mathlib.Data.Finset.Basic
6062
import LeanCamCombi.Mathlib.Data.Finset.Image
63+
import LeanCamCombi.Mathlib.Data.Finset.Insert
6164
import LeanCamCombi.Mathlib.Data.Finset.Lattice.Basic
6265
import LeanCamCombi.Mathlib.Data.Finset.PosDiffs
66+
import LeanCamCombi.Mathlib.Data.Finset.Powerset
6367
import LeanCamCombi.Mathlib.Data.List.DropRight
6468
import LeanCamCombi.Mathlib.Data.Multiset.Basic
6569
import LeanCamCombi.Mathlib.Data.Prod.Lex
70+
import LeanCamCombi.Mathlib.Data.Set.Basic
6671
import LeanCamCombi.Mathlib.Data.Set.Card
72+
import LeanCamCombi.Mathlib.Data.Set.Function
6773
import LeanCamCombi.Mathlib.Data.Set.Image
6874
import LeanCamCombi.Mathlib.Data.Set.Lattice
75+
import LeanCamCombi.Mathlib.Data.Set.Pairwise.Lattice
6976
import LeanCamCombi.Mathlib.Data.Set.Pointwise.Interval
7077
import LeanCamCombi.Mathlib.Data.Set.Pointwise.SMul
7178
import LeanCamCombi.Mathlib.GroupTheory.Coset.Defs

‎LeanCamCombi/Combinatorics/Chap1/Sec1/SCD.lean‎

Lines changed: 115 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,115 @@
1+
/-
2+
Copyright (c) 2022 Yaël Dillies. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Yaël Dillies
5+
-/
6+
import Mathlib.Order.Partition.Finpartition
7+
import LeanCamCombi.Mathlib.Data.Finset.Image
8+
import LeanCamCombi.Mathlib.Data.Finset.Insert
9+
import LeanCamCombi.Mathlib.Data.Finset.Lattice.Basic
10+
11+
/-!
12+
# Symmetric Chain Decompositions
13+
14+
This file shows that if `α` is finite then `Finset α` has a decomposition into symmetric chains,
15+
namely chains of the form `{Cᵢ, ..., Cₙ₋ᵢ}` where `card α = n` and `|C_j| = j`.
16+
-/
17+
18+
namespace Finset
19+
variable {α β : Type*} [DecidableEq α] [DecidableEq β] {s t : Finset α} {f : α → β}
20+
21+
lemma disjoint_image' (hf : Set.InjOn f s) : Disjoint (image f s) (image f t) ↔ Disjoint s t := by
22+
sorry
23+
24+
-- lemma pairwiseDisjoint : s.powerset ∪ 𝒞.image (insert a)
25+
26+
end Finset
27+
28+
open Finset
29+
30+
namespace Finpartition
31+
variable {α : Type*} [DecidableEq α] {𝒜 : Finset (Finset α)} {𝒞 𝒟 : Finset (Finset α)}
32+
{C s : Finset α} {a : α}
33+
34+
def extendExchange (a : α) (𝒞 : Finset (Finset α)) (C : Finset α) : Finset (Finset (Finset α)) :=
35+
if 𝒞.Nontrivial
36+
then {(𝒞 \ {C}).image (insert a), 𝒞 ∪ {insert a C}}
37+
else {𝒞 ∪ {insert a C}}
38+
39+
lemma eq_or_eq_of_mem_extendExchange :
40+
𝒟 ∈ extendExchange a 𝒞 C → 𝒟 = (𝒞 \ {C}).image (insert a) ∨ 𝒟 = 𝒞 ∪ {insert a C} := by
41+
unfold extendExchange; split_ifs with h𝒞 <;> simp (config := { contextual := true })
42+
43+
@[simp] lemma not_empty_mem_extendExchange : ∅ ∉ extendExchange a 𝒞 C := by
44+
unfold extendExchange
45+
split_ifs with h𝒞
46+
· simp [eq_comm (a := ∅), ← nonempty_iff_ne_empty, h𝒞.nonempty.ne_empty, h𝒞.ne_singleton]
47+
· simp [eq_comm (a := ∅), ← nonempty_iff_ne_empty]
48+
49+
@[simp] lemma sup_extendExchange (hC : C ∈ 𝒞) :
50+
(extendExchange a 𝒞 C).sup id = 𝒞 ∪ 𝒞.image (insert a) := by
51+
unfold extendExchange
52+
split_ifs with h𝒞
53+
· simp only [sup_insert, id_eq, sup_singleton, sup_eq_union, union_left_comm]
54+
rw [image_sdiff_of_injOn, image_singleton, sdiff_union_of_subset]
55+
simpa using mem_image_of_mem _ hC
56+
sorry
57+
simpa
58+
· obtain rfl := (eq_singleton_or_nontrivial hC).resolve_right h𝒞
59+
simp
60+
61+
def extendPowersetExchange (P : Finpartition s.powerset) (f : ∀ 𝒞 ∈ P.parts, 𝒞) (a : α)
62+
(ha : a ∉ s) : Finpartition (s.cons a ha).powerset where
63+
64+
-- ofErase
65+
-- (P.parts.attach.biUnion fun ⟨𝒞, h𝒞⟩ ↦ extendExchange a 𝒞 (f 𝒞 h𝒞).1)
66+
-- (by
67+
-- sorry
68+
-- )
69+
-- (by
70+
-- simp
71+
-- )
72+
73+
parts := P.parts.attach.biUnion fun ⟨𝒞, h𝒞⟩ ↦ extendExchange a 𝒞 (f 𝒞 h𝒞).1
74+
supIndep := by
75+
rw [Finset.supIndep_iff_pairwiseDisjoint]
76+
simp only [Set.PairwiseDisjoint, Set.Pairwise, Finset.coe_biUnion, Finset.mem_coe,
77+
Finset.mem_attach, Set.iUnion_true, Set.mem_iUnion, Subtype.exists, ne_eq, Function.onFun,
78+
id_eq, forall_exists_index, not_imp_comm]
79+
rintro x 𝒞 h𝒞 hx y 𝒟 h𝒟 hy hxy
80+
obtain rfl | rfl := eq_or_eq_of_mem_extendExchange hx <;>
81+
obtain rfl | rfl := eq_or_eq_of_mem_extendExchange hy
82+
· rw [disjoint_image'] at hxy
83+
obtain rfl := P.disjoint.elim h𝒞 h𝒟 fun h ↦ hxy $ h.mono sdiff_le sdiff_le
84+
rfl
85+
sorry
86+
· sorry
87+
· sorry
88+
· simp_rw [disjoint_union_left, disjoint_union_right, and_assoc] at hxy
89+
obtain rfl := P.disjoint.elim h𝒞 h𝒟 fun h ↦ hxy $ ⟨h, sorry, sorry, sorry⟩
90+
rfl
91+
sup_parts := by
92+
ext C
93+
simp only [sup_biUnion, coe_mem, sup_extendExchange, mem_sup, mem_attach, mem_union, mem_image,
94+
true_and, Subtype.exists, exists_prop, cons_eq_insert, mem_powerset]
95+
constructor
96+
· rintro ⟨𝒞, h𝒞, hC | ⟨C, hC, rfl⟩⟩
97+
· exact Subset.trans (mem_powerset.1 $ P.le h𝒞 hC) (subset_insert ..)
98+
· exact insert_subset_insert _ (mem_powerset.1 $ P.le h𝒞 hC)
99+
by_cases ha : a ∈ C
100+
· rw [subset_insert_iff]
101+
rintro hC
102+
obtain ⟨𝒞, h𝒞, hC⟩ := P.exists_mem $ mem_powerset.2 hC
103+
exact ⟨𝒞, h𝒞, .inr ⟨_, hC, insert_erase ha⟩⟩
104+
· rw [subset_insert_iff_of_not_mem ha]
105+
rintro hC
106+
obtain ⟨𝒞, h𝒞, hC⟩ := P.exists_mem $ mem_powerset.2 hC
107+
exact ⟨𝒞, h𝒞, .inl hC⟩
108+
not_bot_mem := by simp
109+
110+
/-! ### Profile of a partition -/
111+
112+
/-- The profile of -/
113+
def profile (P : Finpartition s) : Multiset ℕ := P.parts.1.map card
114+
115+
end Finpartition

LeanCamCombi/LittlewoodOfford.lean renamed to LeanCamCombi/Combinatorics/Chap1/Sec1/SDSS.lean

Lines changed: 20 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,26 +1,37 @@
11
/-
22
Copyright (c) 2022 Yaël Dillies. All rights reserved.
3-
Released under Apache 2.0 license as described in the file LICENSE.
3+
Released under Apache 2.0 license as described ∈ the file LICENSE.
44
Authors: Yaël Dillies
55
-/
66
import Mathlib.Analysis.NormedSpace.HahnBanach.Extension
77
import Mathlib.Combinatorics.Enumerative.DoubleCounting
88
import Mathlib.Order.Partition.Finpartition
9+
import LeanCamCombi.Combinatorics.Chap1.Sec1.SCD
910

1011
/-!
11-
# The Littlewood-Offord problem
12+
# Symmetric Decompositions into Sparse Sets
13+
14+
The Littlewood-Offord problem
1215
-/
1316

1417
open scoped BigOperators
1518

1619
namespace Finset
17-
variable {ι E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {𝒜 : Finset (Finset ι)}
18-
{s : Finset ι} {f : ι → E} {r : ℝ}
20+
variable {α E : Type*} {𝒜 : Finset (Finset α)}
21+
{s : Finset α} {f : α → E} {r : ℝ}
22+
23+
def profile (𝒜 : Finset (Finset α)) : Multiset ℕ := sorry
24+
25+
-- def subpartition (f : ):
26+
27+
variable [NormedAddCommGroup E] [NormedSpace ℝ E]
1928

20-
lemma exists_littlewood_offord_partition [DecidableEq ι] (hr : 0 < r) (hf : ∀ i ∈ s, r ≤ ‖f i‖) :
29+
lemma exists_littlewood_offord_partition [DecidableEq α] (hr : 0 < r) (hf : ∀ i ∈ s, r ≤ ‖f i‖) :
2130
∃ P : Finpartition s.powerset,
22-
#P.parts = (#s).choose (#s / 2) ∧ (∀ 𝒜 ∈ P.parts, ∀ t ∈ 𝒜, t ⊆ s) ∧ ∀ 𝒜 ∈ P.parts,
23-
(𝒜 : Set (Finset ι)).Pairwise fun u v ↦ r ≤ dist (∑ i in u, f i) (∑ i in v, f i) := by
31+
#P.parts = (#s).choose (s.card / 2) ∧
32+
(∀ 𝒜 ∈ P.parts, ∀ t ∈ 𝒜, t ⊆ s) ∧
33+
∀ 𝒜 ∈ P.parts,
34+
(𝒜 : Set (Finset α)).Pairwise fun u v ↦ r ≤ dist (∑ i ∈ u, f i) (∑ i ∈ v, f i) := by
2435
classical
2536
induction' s using Finset.induction with i s hi ih
2637
· exact ⟨Finpartition.indiscrete $ singleton_ne_empty _, by simp⟩
@@ -29,12 +40,12 @@ lemma exists_littlewood_offord_partition [DecidableEq ι] (hr : 0 < r) (hf : ∀
2940
obtain ⟨g, hg, hgf⟩ :=
3041
exists_dual_vector ℝ (f i) (norm_pos_iff.1 $ hr.trans_le $ hf _ $ mem_insert_self _ _)
3142
choose! t ht using fun 𝒜 (h𝒜 : 𝒜 ∈ P.parts) ↦
32-
Finset.exists_max_image _ (fun t ↦ g (∑ i in t, f i)) (P.nonempty_of_mem_parts h𝒜)
43+
Finset.exists_max_image _ (fun t ↦ g (∑ i ∈ t, f i)) (P.nonempty_of_mem_parts h𝒜)
3344
sorry
3445

3546
/-- **Kleitman's lemma** -/
3647
lemma card_le_of_forall_dist_sum_le (hr : 0 < r) (h𝒜 : ∀ t ∈ 𝒜, t ⊆ s) (hf : ∀ i ∈ s, r ≤ ‖f i‖)
37-
(h𝒜r : ∀ u, u ∈ 𝒜 → ∀ v, v ∈ 𝒜 → dist (∑ i in u, f i) (∑ i in v, f i) < r) :
48+
(h𝒜r : ∀ u, u ∈ 𝒜 → ∀ v, v ∈ 𝒜 → dist (∑ i ∈ u, f i) (∑ i ∈ v, f i) < r) :
3849
#𝒜 ≤ (#s).choose (#s / 2) := by
3950
classical
4051
obtain ⟨P, hP, _hs, hr⟩ := exists_littlewood_offord_partition hr hf

‎LeanCamCombi/Mathlib/Data/Finset/Basic.lean‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
import Mathlib.Data.Finset.Basic
2+
3+
namespace Finset
4+
variable {α : Type*} {a : α} {s t : Finset α}
5+
6+
lemma not_mem_subset (h : s ⊆ t) : a ∉ t → a ∉ s := Set.not_mem_subset h
7+
8+
end Finset
9+
10+
namespace Finset
11+
variable {ι α : Type*} [DecidableEq α] {s : Set ι} {f : ι → Finset α}
12+
13+
lemma pairwiseDisjoint_iff :
14+
s.PairwiseDisjoint f ↔ ∀ ⦃i⦄, i ∈ s → ∀ ⦃j⦄, j ∈ s → (f i ∩ f j).Nonempty → i = j := by
15+
simp [Set.PairwiseDisjoint, Set.Pairwise, Function.onFun, not_imp_comm (a := _ = _),
16+
not_disjoint_iff_nonempty_inter]
17+
18+
end Finset

‎LeanCamCombi/Mathlib/Data/Finset/Image.lean‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
11
import Mathlib.Data.Finset.Image
2+
import LeanCamCombi.Mathlib.Data.Set.Function
23

34
namespace Finset
45
variable {α β : Type*} [DecidableEq β] {f : α → β} {s : Finset α} {p : β → Prop}
@@ -7,3 +8,12 @@ lemma forall_mem_image : (∀ y ∈ s.image f, p y) ↔ ∀ ⦃x⦄, x ∈ s →
78
lemma exists_mem_image : (∃ y ∈ s.image f, p y) ↔ ∃ x ∈ s, p (f x) := by simp
89

910
end Finset
11+
12+
namespace Finset
13+
variable {α β : Type*} [DecidableEq α] [DecidableEq β] {s t : Finset α} {f : α → β}
14+
15+
lemma image_sdiff_of_injOn (hf : Set.InjOn f s) (hts : t ⊆ s) :
16+
(s \ t).image f = s.image f \ t.image f :=
17+
mod_cast Set.image_diff_of_injOn hf <| coe_subset.2 hts
18+
19+
end Finset

‎LeanCamCombi/Mathlib/Data/Finset/Insert.lean‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
import Mathlib.Data.Finset.Insert
2+
3+
namespace Finset
4+
variable {α : Type*} [DecidableEq α]
5+
6+
instance Nontrivial.instDecidablePred : DecidablePred (Finset.Nontrivial (α := α)) :=
7+
inferInstanceAs (DecidablePred fun s ↦ ∃ a ∈ s, ∃ b ∈ s, a ≠ b)
8+
9+
end Finset

‎LeanCamCombi/Mathlib/Data/Finset/Lattice/Basic.lean‎

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,10 @@
1+
import Mathlib.Data.Finset.Empty
12
import Mathlib.Data.Finset.Lattice.Basic
23

34
namespace Finset
5+
variable {α : Type*} [DecidableEq α] {s t : Finset α}
46

5-
attribute [simp] inter_subset_left inter_subset_right
7+
@[simp] lemma union_nonempty : (s ∪ t).Nonempty ↔ s.Nonempty ∨ t.Nonempty :=
8+
mod_cast Set.union_nonempty (α := α) (s := s) (t := t)
69

710
end Finset

‎LeanCamCombi/Mathlib/Data/Finset/Powerset.lean‎

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
import Mathlib.Data.Finset.Powerset
2+
import LeanCamCombi.Mathlib.Data.Finset.Basic
3+
import LeanCamCombi.Mathlib.Data.Set.Pairwise.Lattice
4+
5+
namespace Finset
6+
variable {α : Type*} [DecidableEq α] {s : Finset α} {a : α}
7+
8+
lemma pairwiseDisjoint_pair_insert (ha : a ∉ s) :
9+
(s.powerset : Set (Finset α)).PairwiseDisjoint
10+
fun t ↦ ({t, insert a t} : Set (Finset α)) := by
11+
simp_rw [Set.pairwiseDisjoint_iff, mem_coe, mem_powerset]
12+
rintro i hi j hj
13+
simp only [Set.Nonempty, Set.mem_inter_iff, Set.mem_insert_iff, Set.mem_singleton_iff,
14+
exists_eq_or_imp, exists_eq_left, or_imp, imp_self, true_and]
15+
refine ⟨?_, ?_, insert_erase_invOn.2.injOn (not_mem_mono hi ha) (not_mem_mono hj ha)⟩ <;>
16+
rintro rfl <;>
17+
cases Finset.not_mem_subset ‹_› ha (Finset.mem_insert_self _ _)
18+
19+
end Finset

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

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
import Mathlib.Data.Set.Basic
2+
3+
namespace Set
4+
variable {α : Type*} {s : Set α} {a : α}
5+
6+
lemma insert_diff_self_of_mem (ha : a ∈ s) : insert a (s \ {a}) = s := by aesop
7+
8+
lemma insert_erase_invOn :
9+
InvOn (insert a) (fun s ↦ s \ {a}) {s : Set α | a ∈ s} {s : Set α | a ∉ s} :=
10+
⟨fun _s ha ↦ insert_diff_self_of_mem ha, fun _s ↦ insert_diff_self_of_not_mem⟩
11+
12+
end Set

‎LeanCamCombi/Mathlib/Data/Set/Function.lean‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
import Mathlib.Data.Set.Function
2+
3+
namespace Set
4+
5+
-- TODO: Rename
6+
alias image_diff_of_injOn := InjOn.image_diff_subset
7+
8+
end Set

0 commit comments

Comments
 (0)