Formalizing Structural Graph Theory in Lean 4

Dev/MonadicDependence/BipartiteRamsey/Full.lean
1import Mathlib.Data.Finset.Card
2import Mathlib.Data.Finset.Sort
3import Mathlib.Data.Fin.Tuple.Basic
4import Mathlib.Data.Fintype.Pi
5import Mathlib.Combinatorics.Pigeonhole
6import Mathlib.Order.Monotone.Basic
7import Catalog.Sparsity.Preliminaries.Full
8
9namespace Dev.MonadicDependence.BipartiteRamsey
10
11/-- Order type of a tuple `a : Fin ℓ → V` (`V` linearly ordered). For
12each pair `(i, j) : Fin ℓ × Fin ℓ`, records whether `a i < a j`,
13`a i = a j`, or `a i > a j`. Mählmann p. 28 writes this as `otp(a)`. -/
14def orderType {V : Type*} [LinearOrder V] {ℓ : ℕ} (a : Fin ℓ → V) :
15 Fin ℓ × Fin ℓ → Ordering :=
16 fun p => compare (a p.1) (a p.2)
17
18section Helpers
19
20/-- Generic packaging helper: convert a size-indexed Ramsey bound into the
21monotone-unbounded form used throughout the entry.
22
23Given a property `P n M` trivial at `M = 0` and a bound function `Nfin`
24with `Nfin M ≤ n → P n M`, produce a monotone unbounded `N : ℕ → ℕ` with
25`P n (N n)` for all `n`. The bound `N` is the largest `M ≤ n` with
26`Nfin' M ≤ n`, where `Nfin'` is a monotone envelope of `Nfin`. -/
27private lemma existsMonotoneUnbounded {P : ℕ → ℕ → Prop}
28 (hP_zero : ∀ n, P n 0)
29 (Nfin : ℕ → ℕ) (hNfin : ∀ M n, Nfin M ≤ n → P n M) :
30 ∃ N : ℕ → ℕ, Monotone N ∧ (∀ K : ℕ, ∃ n, K ≤ N n) ∧ ∀ n, P n (N n) := by
31 classical
32 let Nfin' : ℕ → ℕ := fun M =>
33 (Finset.range (M + 1)).sup (fun M' => max M' (Nfin M'))
34 have hNfin'_mono : Monotone Nfin' := by
35 intro a b hab
36 apply Finset.sup_mono
37 intro x hx
38 simp only [Finset.mem_range] at hx ⊢
39 omega
40 have hNfin'_geId : ∀ M, M ≤ Nfin' M := by
41 intro M
42 have h1 : M ≤ max M (Nfin M) := le_max_left _ _
43 have h2 : max M (Nfin M) ≤ Nfin' M := by
44 apply Finset.le_sup (f := fun M' => max M' (Nfin M'))
45 (s := Finset.range (M + 1))
46 exact Finset.self_mem_range_succ M
47 exact h1.trans h2
48 have hNfin'_geNfin : ∀ M, Nfin M ≤ Nfin' M := by
49 intro M
50 have h1 : Nfin M ≤ max M (Nfin M) := le_max_right _ _
51 have h2 : max M (Nfin M) ≤ Nfin' M := by
52 apply Finset.le_sup (f := fun M' => max M' (Nfin M'))
53 (s := Finset.range (M + 1))
54 exact Finset.self_mem_range_succ M
55 exact h1.trans h2
56 refine ⟨fun n => Nat.findGreatest (fun M => Nfin' M ≤ n) n, ?_, ?_, ?_⟩
57 · intro a b hab
58 refine Nat.findGreatest_mono ?_ hab
59 intro M hM
60 exact hM.trans hab
61 · intro K
62 refine ⟨Nfin' K, ?_⟩
63 exact Nat.le_findGreatest (hNfin'_geId K) le_rfl
64 · intro n
65 show P n (Nat.findGreatest (fun M => Nfin' M ≤ n) n)
66 by_cases h : Nfin' 0 ≤ n
67 · have hspec : Nfin' (Nat.findGreatest (fun M => Nfin' M ≤ n) n) ≤ n :=
68 Nat.findGreatest_spec (P := fun M => Nfin' M ≤ n) (Nat.zero_le n) h
69 exact hNfin _ n ((hNfin'_geNfin _).trans hspec)
70 · push_neg at h
71 have hzero : Nat.findGreatest (fun M => Nfin' M ≤ n) n = 0 := by
72 rw [Nat.findGreatest_eq_zero_iff]
73 intro k hk0 _
74 have : Nfin' 0 ≤ Nfin' k := hNfin'_mono (Nat.zero_le k)
75 omega
76 rw [hzero]
77 exact hP_zero n
78
79/-- Chain-building bound for the strict-monotone Ramsey induction.
80Given a per-size bound `ih : ℕ → ℕ`, `chainBound ih T` is the size needed
81to perform `T` iterations of the Erdős–Rado chain-building step. -/
82private def chainBound : (ℕ → ℕ) → ℕ → ℕ
83 | _, 0 => 0
84 | ih, T + 1 => ih (chainBound ih T) + 1
85
86/-- Chain-building step for the strict-monotone hypergraph Ramsey induction.
87Given an `(m'-tuple)`-level Ramsey bound `ih_fn`, build for each `T : ℕ` a
88set `I ⊆ S` of size `T` together with a coloring `cols` of its elements
89such that every strict-monotone `(m'+1)`-tuple from `I` has color
90`cols (a 0)` (the color of its minimum). -/
91private lemma buildChain (k m' : ℕ) (ih_fn : ℕ → ℕ)
92 (ih_spec : ∀ (r : ℕ) {n : ℕ} (S : Finset (Fin n)),
93 ih_fn r ≤ S.card → ∀ c : (Fin m' → Fin n) → Fin k,
94 ∃ I : Finset (Fin n), I ⊆ S ∧ r ≤ I.card ∧ ∃ col : Fin k,
95 ∀ a : Fin m' → Fin n, StrictMono a → (∀ i, a i ∈ I) → c a = col) :
96 ∀ (T : ℕ) {n : ℕ} (S : Finset (Fin n))
97 (c : (Fin (m' + 1) → Fin n) → Fin k),
98 chainBound ih_fn T ≤ S.card →
99 ∃ I : Finset (Fin n), I ⊆ S ∧ T ≤ I.card ∧
100 ∃ cols : Fin n → Fin k,
101 ∀ a : Fin (m' + 1) → Fin n, StrictMono a → (∀ i, a i ∈ I) →
102 c a = cols (a 0) := by
103 classical
104 intro T
105 induction T with
106 | zero =>
107 intro n S c _
108 refine ⟨∅, Finset.empty_subset _, ?_, fun x => c (fun _ => x), ?_⟩
109 · simp
110 · intro a _ hmem
111 exact absurd (hmem 0) (Finset.notMem_empty _)
112 | succ T' ihT =>
113 intro n S c hS
114 have hSpos : 0 < S.card := by
115 change ih_fn (chainBound ih_fn T') + 1 ≤ S.card at hS
116 omega
117 have hSne : S.Nonempty := Finset.card_pos.mp hSpos
118 let v : Fin n := S.min' hSne
119 have hvmem : v ∈ S := S.min'_mem hSne
120 let S₁ : Finset (Fin n) := S.erase v
121 have hS₁card : ih_fn (chainBound ih_fn T') ≤ S₁.card := by
122 have h1 : S₁.card = S.card - 1 :=
123 Finset.card_erase_of_mem hvmem
124 change ih_fn (chainBound ih_fn T') + 1 ≤ S.card at hS
125 omega
126 let c' : (Fin m' → Fin n) → Fin k := fun b => c (Fin.cons v b)
127 obtain ⟨J, hJsub, hJcard, col_v, hJhomo⟩ :=
128 ih_spec (chainBound ih_fn T') S₁ hS₁card c'
129 obtain ⟨I', hI'sub, hI'card, cols', hI'homo⟩ := ihT J c hJcard
130 have hvNotI' : v ∉ I' := by
131 intro hv
132 have hvJ : v ∈ J := hI'sub hv
133 have hvS₁ : v ∈ S₁ := hJsub hvJ
134 exact (Finset.notMem_erase v S) hvS₁
135 have hvLT : ∀ x ∈ S, x ≠ v → v < x := by
136 intro x hxS hxne
137 have hle : v ≤ x := S.min'_le x hxS
138 exact lt_of_le_of_ne hle (Ne.symm hxne)
139 refine ⟨insert v I', ?_, ?_, ?_⟩
140 · -- insert v I' ⊆ S
141 intro x hx
142 rcases Finset.mem_insert.mp hx with rfl | hxI'
143 · exact hvmem
144 · have hxS₁ : x ∈ S₁ := hJsub (hI'sub hxI')
145 exact (Finset.mem_erase.mp hxS₁).2
146 · -- T'+1 ≤ |insert v I'|
147 rw [Finset.card_insert_of_notMem hvNotI']
148 omega
149 · -- Homogeneity.
150 refine ⟨fun x => if x = v then col_v else cols' x, ?_⟩
151 intro a ha hmem
152 by_cases h0 : a 0 = v
153 · -- Case: a 0 = v. Tail lives in I'.
154 have h_tail_mem : ∀ i : Fin m', (Fin.tail a) i ∈ I' := by
155 intro i
156 have hmem_succ : a i.succ ∈ insert v I' := hmem i.succ
157 have hne : a i.succ ≠ v := by
158 have hlt : a 0 < a i.succ := ha (Fin.succ_pos i)
159 rw [h0] at hlt
160 exact ne_of_gt hlt
161 rcases Finset.mem_insert.mp hmem_succ with heq | hI'
162 · exact absurd heq hne
163 · exact hI'
164 have h_tail_strict : StrictMono (Fin.tail a) := by
165 intro i j hij
166 exact ha (Fin.succ_lt_succ_iff.mpr hij)
167 have h_tail_J : ∀ i, (Fin.tail a) i ∈ J := fun i =>
168 hI'sub (h_tail_mem i)
169 have hc' : c (Fin.cons v (Fin.tail a)) = col_v :=
170 hJhomo (Fin.tail a) h_tail_strict h_tail_J
171 have h_eq : a = Fin.cons v (Fin.tail a) := by
172 apply funext
173 intro i
174 refine Fin.cases ?_ ?_ i
175 · simp [Fin.cons_zero, h0]
176 · intro j; simp [Fin.cons_succ, Fin.tail]
177 have : c a = col_v := by rw [h_eq]; exact hc'
178 simp [h0, this]
179 · -- Case: a 0 ≠ v. Whole image lives in I'.
180 have h_mem_I' : ∀ i, a i ∈ I' := by
181 intro i
182 have hmem_i : a i ∈ insert v I' := hmem i
183 by_cases hi : i = 0
184 · subst hi
185 rcases Finset.mem_insert.mp hmem_i with heq | hI'
186 · exact absurd heq h0
187 · exact hI'
188 · -- a i > a 0 > v, so a i ≠ v
189 have h_a0_S : a 0 ∈ S := by
190 have : a 0 ∈ insert v I' := hmem 0
191 rcases Finset.mem_insert.mp this with heq | hI'
192 · rw [heq]; exact hvmem
193 · have hS₁ : a 0 ∈ S₁ := hJsub (hI'sub hI')
194 exact (Finset.mem_erase.mp hS₁).2
195 have hv_lt_a0 : v < a 0 := hvLT (a 0) h_a0_S h0
196 have h_a0_lt_ai : a 0 < a i := ha (Fin.pos_of_ne_zero hi)
197 have hne : a i ≠ v := ne_of_gt (lt_trans hv_lt_a0 h_a0_lt_ai)
198 rcases Finset.mem_insert.mp hmem_i with heq | hI'
199 · exact absurd heq hne
200 · exact hI'
201 have hc' : c a = cols' (a 0) := hI'homo a ha h_mem_I'
202 have h_a0_ne_v : a 0 ≠ v := h0
203 simp [h_a0_ne_v, hc']
204
205/-- Hypergraph Ramsey for strict-monotone `m`-tuples (Finset form).
206Given a finite subset `S` of `Fin n` large enough, every `k`-coloring of
207strict-monotone `m`-tuples from `Fin n` has a monochromatic subset of `S`
208of size `M`. Proved by induction on `m` via Erdős–Rado. -/
209private lemma strictMonoRamseyFinset (k : ℕ) :
210 ∀ (m M : ℕ), ∃ Nfin : ℕ, ∀ {n : ℕ} (S : Finset (Fin n)),
211 Nfin ≤ S.card → ∀ c : (Fin m → Fin n) → Fin k,
212 ∃ I : Finset (Fin n), I ⊆ S ∧ M ≤ I.card ∧ ∃ col : Fin k,
213 ∀ a : Fin m → Fin n, StrictMono a → (∀ i, a i ∈ I) → c a = col := by
214 intro m
215 induction m with
216 | zero =>
217 intro M
218 refine ⟨M, ?_⟩
219 intro n S hS c
220 refine ⟨S, Finset.Subset.refl _, hS, c Fin.elim0, ?_⟩
221 intro a _ _
222 have : a = Fin.elim0 := funext (fun i => Fin.elim0 i)
223 rw [this]
224 | succ m' ih =>
225 classical
226 intro M
227 -- Extract ih as a function.
228 let ih_fn : ℕ → ℕ := fun r => (ih r).choose
229 have ih_spec : ∀ (r : ℕ) {n : ℕ} (S : Finset (Fin n)),
230 ih_fn r ≤ S.card → ∀ c : (Fin m' → Fin n) → Fin k,
231 ∃ I : Finset (Fin n), I ⊆ S ∧ r ≤ I.card ∧ ∃ col : Fin k,
232 ∀ a : Fin m' → Fin n, StrictMono a →
233 (∀ i, a i ∈ I) → c a = col :=
234 fun r => (ih r).choose_spec
235 -- T = M · k + 1 rounds (loose; M·k gives pigeonhole M occurrences).
236 let T : ℕ := M * k + 1
237 refine ⟨chainBound ih_fn T, ?_⟩
238 intro n S hS c
239 obtain ⟨I, hIsub, hIcard, cols, hIhomo⟩ :=
240 buildChain k m' ih_fn ih_spec T S c hS
241 -- Pigeonhole on `cols` restricted to `I`.
242 have hcard_lt : k * M < I.card := by
243 have : T ≤ I.card := hIcard
244 have : M * k + 1 ≤ I.card := this
245 have hmk : M * k = k * M := Nat.mul_comm _ _
246 omega
247 -- There is a color appearing more than `M` times in `I`.
248 have : ∃ col : Fin k, M < (I.filter (fun x => cols x = col)).card := by
249 by_contra hneg
250 push_neg at hneg
251 -- Sum of (filter).card = I.card (since every elt of I has some color).
252 have hsum : ∑ col : Fin k, (I.filter (fun x => cols x = col)).card
253 = I.card := by
254 have := @Finset.card_eq_sum_card_fiberwise _ _ _ cols I
255 Finset.univ (fun x _ => Finset.mem_univ _)
256 simpa using this.symm
257 have hbound : ∑ col : Fin k, (I.filter (fun x => cols x = col)).card
258 ≤ k * M := by
259 calc ∑ col : Fin k, (I.filter (fun x => cols x = col)).card
260 ≤ ∑ _col : Fin k, M := Finset.sum_le_sum (fun col _ => hneg col)
261 _ = k * M := by simp [Finset.sum_const, Finset.card_univ]
262 omega
263 obtain ⟨col, hcol⟩ := this
264 refine ⟨I.filter (fun x => cols x = col), ?_, ?_, col, ?_⟩
265 · exact (Finset.filter_subset _ _).trans hIsub
266 · exact hcol.le
267 · intro a ha hmem
268 have hmemI : ∀ i, a i ∈ I := fun i =>
269 (Finset.mem_filter.mp (hmem i)).1
270 have ha0_col : cols (a 0) = col :=
271 (Finset.mem_filter.mp (hmem 0)).2
272 rw [hIhomo a ha hmemI, ha0_col]
273
274private def Shape (ℓ : ℕ) :=
275 Σ m : Fin (ℓ + 1), {σ : Fin ℓ → Fin m.1 // Function.Surjective σ}
276
277private def Shape.arity {ℓ : ℕ} (s : Shape ℓ) : ℕ :=
278 s.1.1
279
280private def Shape.pattern {ℓ : ℕ} (s : Shape ℓ) : Fin ℓ → Fin s.arity :=
281 s.2.1
282
283private lemma Shape.pattern_surjective {ℓ : ℕ} (s : Shape ℓ) :
284 Function.Surjective s.pattern :=
285 s.2.2
286
287private instance shapeFintype (ℓ : ℕ) : Fintype (Shape ℓ) := by
288 classical
289 unfold Shape
290 infer_instance
291
292private lemma orderType_comp_strictMono {α β : Type*} [LinearOrder α] [LinearOrder β]
293 {ℓ : ℕ} {σ : Fin ℓ → α} {e : α → β} (he : StrictMono e) :
294 orderType (e ∘ σ) = orderType σ := by
295 ext p
296 rcases lt_trichotomy (σ p.1) (σ p.2) with hlt | heq | hgt
297 · simp [orderType, Function.comp, compare_lt_iff_lt.mpr hlt,
298 compare_lt_iff_lt.mpr (he hlt)]
299 · simp [orderType, Function.comp, heq]
300 · simp [orderType, Function.comp, compare_gt_iff_gt.mpr hgt,
301 compare_gt_iff_gt.mpr (he hgt)]
302
303private lemma factorThroughShape {ℓ m n : ℕ} {σ : Fin ℓ → Fin m}
304 (hσsurj : Function.Surjective σ) (a : Fin ℓ → Fin n)
305 (hot : orderType σ = orderType a) :
306 ∃ e : Fin m → Fin n, StrictMono e ∧ a = e ∘ σ := by
307 classical
308 let τ : Fin m → Fin ℓ := fun r => Classical.choose (hσsurj r)
309 have hτ : Function.RightInverse τ σ := fun r => Classical.choose_spec (hσsurj r)
310 let e : Fin m → Fin n := fun r => a (τ r)
311 have he : StrictMono e := by
312 intro r s hrs
313 have hcmp : compare (e r) (e s) = Ordering.lt := by
314 simpa [e, orderType, hτ r, hτ s, compare_lt_iff_lt.mpr hrs] using
315 (congrArg (fun ot => ot (τ r, τ s)) hot).symm
316 exact compare_lt_iff_lt.mp hcmp
317 refine ⟨e, he, funext fun i => ?_⟩
318 have hcmp0 : compare (a i) (a (τ (σ i))) = compare (σ i) (σ (τ (σ i))) := by
319 simpa [orderType] using (congrArg (fun ot => ot (i, τ (σ i))) hot).symm
320 have hcmp : compare (a i) (e (σ i)) = Ordering.eq := by
321 simpa [e, hτ (σ i)] using hcmp0
322 exact compare_eq_iff_eq.mp hcmp
323
324private lemma decomposeTuple {ℓ n : ℕ} (a : Fin ℓ → Fin n) :
325 ∃ s : Shape ℓ, ∃ e : Fin s.arity → Fin n, StrictMono e ∧ a = e ∘ s.pattern := by
326 classical
327 let A : Finset (Fin n) := Finset.univ.image a
328 have hAcard : A.card ≤ ℓ := by
329 simpa [A] using (Finset.card_image_le (s := (Finset.univ : Finset (Fin ℓ))) (f := a))
330 let m : Fin (ℓ + 1) := ⟨A.card, Nat.lt_succ_of_le hAcard⟩
331 let emb : Fin m.1 ↪o Fin n := A.orderEmbOfFin rfl
332 have ha_mem_range : ∀ i : Fin ℓ, a i ∈ Finset.image emb Finset.univ := by
333 intro i
334 have : a i ∈ A := by
335 refine Finset.mem_image.mpr ?_
336 exact ⟨i, Finset.mem_univ _, rfl⟩
337 simpa [A, emb] using this
338 have hpre : ∀ i : Fin ℓ, ∃ j : Fin m.1, emb j = a i := by
339 intro i
340 rcases Finset.mem_image.mp (ha_mem_range i) with ⟨j, _, hj⟩
341 exact ⟨j, hj⟩
342 choose σ hσ using hpre
343 have hσsurj : Function.Surjective σ := by
344 intro j
345 have hjA : emb j ∈ A := Finset.orderEmbOfFin_mem A rfl j
346 have hjim : emb j ∈ Finset.univ.image a := by simpa [A] using hjA
347 rcases Finset.mem_image.mp hjim with ⟨i, -, hi⟩
348 refine ⟨i, ?_⟩
349 apply emb.injective
350 simpa [hσ i] using hi
351 let s : Shape ℓ := ⟨m, ⟨σ, hσsurj⟩⟩
352 refine ⟨s, emb, emb.strictMono, ?_⟩
353 ext i
354 exact congrArg Fin.val (hσ i).symm
355
356private lemma shapeRamseyFamily (k ℓ M : ℕ) (hk : 0 < k) :
357 ∀ T : Finset (Shape ℓ), ∃ Nfin : ℕ, ∀ {n : ℕ} (S : Finset (Fin n)),
358 Nfin ≤ S.card → ∀ c : (Fin ℓ → Fin n) → Fin k,
359 ∃ I : Finset (Fin n), I ⊆ S ∧ M ≤ I.card ∧
360 ∃ cols : Shape ℓ → Fin k,
361 ∀ s ∈ T, ∀ e : Fin s.arity → Fin n, StrictMono e →
362 (∀ i, e i ∈ I) → c (e ∘ s.pattern) = cols s := by
363 intro T
364 classical
365 refine Finset.induction_on T ?_ ?_
366 · refine ⟨M, ?_⟩
367 intro n S hS c
368 refine ⟨S, Finset.Subset.rfl, hS, fun _ => ⟨0, by omega⟩, ?_⟩
369 intro s hs
370 exact False.elim (Finset.notMem_empty _ hs)
371 · intro s T hs ih
372 obtain ⟨NT, hT⟩ := ih
373 obtain ⟨Ns, hspec⟩ := strictMonoRamseyFinset k s.arity NT
374 refine ⟨Ns, ?_⟩
375 intro n S hS c
376 obtain ⟨J, hJsub, hJcard, col_s, hJhom⟩ :=
377 hspec S hS (fun e => c (e ∘ s.pattern))
378 obtain ⟨I, hIsub, hIcard, colsT, hIhom⟩ :=
379 hT J hJcard c
380 refine ⟨I, hIsub.trans hJsub, hIcard, Function.update colsT s col_s, ?_⟩
381 intro t ht e he hemem
382 rcases Finset.mem_insert.mp ht with rfl | htT
383 · simp [Function.update]
384 exact hJhom e he (fun i => hIsub (hemem i))
385 · have hts : t ≠ s := by
386 intro hts
387 subst hts
388 exact hs htT
389 simp [Function.update, hts]
390 exact hIhom t htT e he hemem
391
392/-- Hypergraph Ramsey at a given size, for arbitrary (not necessarily
393strict-monotone) `ℓ`-tuples with order-type homogeneity.
394
395**Proof strategy (not yet formalized).** Given a `k`-coloring
396`c : (Fin ℓ → Fin n) → Fin k`, factor each tuple `a : Fin ℓ → V` through
397its rank pattern: `a = ã ∘ σ` with `σ : Fin ℓ → Fin m` (`m ≤ ℓ`, the
398number of distinct values of `a`) and `ã : Fin m → V` strict-monotone.
399The pair `(m, σ)` is fully determined by `orderType a`.
400
401Iterate `strictMonoRamseyFinset` over the finite shape type
402`Σ m : Fin (ℓ+1), Fin ℓ → Fin m.val`: for each shape `(m, σ)`, apply
403`strictMonoRamseyFinset k m _` to the induced coloring
404`c_σ ã := c (ã ∘ σ)` and shrink `S`. After all shapes are processed,
405define `f : orderType → Fin k` by looking up the color assigned to the
406shape induced by each order type. -/
407private lemma tupleRamseyAtSize (k ℓ M : ℕ) (hk : 0 < k) :
408 ∃ Nfin : ℕ, ∀ {n : ℕ} (S : Finset (Fin n)),
409 Nfin ≤ S.card → ∀ c : (Fin ℓ → Fin n) → Fin k,
410 ∃ I : Finset (Fin n), I ⊆ S ∧ M ≤ I.card ∧
411 ∃ f : (Fin ℓ × Fin ℓ → Ordering) → Fin k,
412 ∀ a : Fin ℓ → Fin n, (∀ i, a i ∈ I) → c a = f (orderType a) := by
413 classical
414 obtain ⟨Nfin, hNfin⟩ := shapeRamseyFamily k ℓ M hk (Finset.univ : Finset (Shape ℓ))
415 refine ⟨Nfin, ?_⟩
416 intro n S hS c
417 obtain ⟨I, hIsub, hIcard, cols, hIhom⟩ := hNfin S hS c
418 refine ⟨I, hIsub, hIcard, ?_⟩
419 refine ⟨fun ot => if h : ∃ s : Shape ℓ, orderType s.pattern = ot then cols (Classical.choose h)
420 else ⟨0, hk⟩, ?_⟩
421 intro a hmem
422 have hex : ∃ s : Shape ℓ, orderType s.pattern = orderType a := by
423 obtain ⟨s, e, he, hfac⟩ := decomposeTuple a
424 refine ⟨s, ?_⟩
425 simpa [hfac] using (orderType_comp_strictMono (σ := s.pattern) he).symm
426 let s : Shape ℓ := Classical.choose hex
427 have hs_ot : orderType s.pattern = orderType a := Classical.choose_spec hex
428 obtain ⟨e, he, hfac⟩ := factorThroughShape s.pattern_surjective a hs_ot
429 have hemem : ∀ i, e i ∈ I := by
430 intro i
431 rcases s.pattern_surjective i with ⟨j, rfl⟩
432 simpa [hfac] using hmem j
433 have hc : c a = cols s := by
434 rw [hfac]
435 exact hIhom s (by simp) e he hemem
436 simpa [hex] using hc
437
438theorem tupleRamsey (k ℓ : ℕ) (hk : 0 < k) :
439 ∃ N : ℕ → ℕ, Monotone N ∧ (∀ M : ℕ, ∃ n : ℕ, M ≤ N n) ∧
440 ∀ (n : ℕ) (c : (Fin ℓ → Fin n) → Fin k),
441 ∃ I : Finset (Fin n), N n ≤ I.card ∧
442 ∃ f : (Fin ℓ × Fin ℓ → Ordering) → Fin k,
443 ∀ (a : Fin ℓ → Fin n), (∀ i, a i ∈ I) →
444 c a = f (orderType a) := by
445 -- Package `tupleRamseyAtSize` into the monotone-unbounded form via
446 -- `existsMonotoneUnbounded`.
447 classical
448 let P : ℕ → ℕ → Prop := fun n M =>
449 ∀ c : (Fin ℓ → Fin n) → Fin k,
450 ∃ I : Finset (Fin n), M ≤ I.card ∧
451 ∃ f : (Fin ℓ × Fin ℓ → Ordering) → Fin k,
452 ∀ a : Fin ℓ → Fin n, (∀ i, a i ∈ I) → c a = f (orderType a)
453 have hP_zero : ∀ n, P n 0 := by
454 intro n c
455 by_cases hℓ : ℓ = 0
456 · subst hℓ
457 refine ⟨∅, by simp, fun _ => c Fin.elim0, ?_⟩
458 intro a _
459 have : a = Fin.elim0 := funext (fun i => Fin.elim0 i)
460 rw [this]
461 · obtain ⟨m, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hℓ
462 refine ⟨∅, by simp, fun _ => ⟨0, hk⟩, ?_⟩
463 intro a hmem
464 exact absurd (hmem 0) (Finset.notMem_empty _)
465 let Nfin : ℕ → ℕ := fun M => (tupleRamseyAtSize k ℓ M hk).choose
466 have hNfin : ∀ M n, Nfin M ≤ n → P n M := by
467 intro M n hn c
468 obtain ⟨I, hIsub, hIcard, f, hf⟩ :=
469 (tupleRamseyAtSize k ℓ M hk).choose_spec (S := (Finset.univ : Finset (Fin n))) (by simpa using hn) c
470 exact ⟨I, hIcard, f, hf⟩
471 obtain ⟨N, hNmono, hNunb, hN⟩ := existsMonotoneUnbounded hP_zero Nfin hNfin
472 refine ⟨N, hNmono, hNunb, ?_⟩
473 intro n c
474 exact hN n c
475
476/-- Glue two order types of `ℓ₁`- and `ℓ₂`-tuples into an order type of
477a `(ℓ₁ + ℓ₂)`-tuple, assuming (virtually) that every entry of the first
478tuple is strictly less than every entry of the second. Cross-coordinates
479are set to `.lt` (left-right) or `.gt` (right-left). -/
480def glueLT {ℓ₁ ℓ₂ : ℕ}
481 (ot₁ : Fin ℓ₁ × Fin ℓ₁ → Ordering)
482 (ot₂ : Fin ℓ₂ × Fin ℓ₂ → Ordering) :
483 Fin (ℓ₁ + ℓ₂) × Fin (ℓ₁ + ℓ₂) → Ordering :=
484 fun p => Fin.addCases
485 (fun i₁ => Fin.addCases
486 (fun j₁ => ot₁ (i₁, j₁))
487 (fun _ => Ordering.lt)
488 p.2)
489 (fun i₂ => Fin.addCases
490 (fun _ => Ordering.gt)
491 (fun j₂ => ot₂ (i₂, j₂))
492 p.2)
493 p.1
494
495/-- When every coordinate of `a` is strictly less than every coordinate
496of `b`, the order type of the concatenation `Fin.append a b` factors
497through the pair `(orderType a, orderType b)` via `glueLT`. -/
498lemma orderType_append_of_lt {V : Type*} [LinearOrder V]
499 {ℓ₁ ℓ₂ : ℕ} {a : Fin ℓ₁ → V} {b : Fin ℓ₂ → V}
500 (hab : ∀ (i : Fin ℓ₁) (j : Fin ℓ₂), a i < b j) :
501 orderType (Fin.append a b) = glueLT (orderType a) (orderType b) := by
502 ext ⟨i, j⟩
503 refine Fin.addCases (fun i₁ => ?_) (fun i₂ => ?_) i
504 · refine Fin.addCases (fun j₁ => ?_) (fun j₂ => ?_) j
505 · simp [orderType, glueLT, Fin.append_left, Fin.addCases_left]
506 · simp only [orderType, glueLT, Fin.append_left, Fin.append_right,
507 Fin.addCases_left, Fin.addCases_right]
508 exact compare_lt_iff_lt.mpr (hab i₁ j₂)
509 · refine Fin.addCases (fun j₁ => ?_) (fun j₂ => ?_) j
510 · simp only [orderType, glueLT, Fin.append_left, Fin.append_right,
511 Fin.addCases_left, Fin.addCases_right]
512 exact compare_gt_iff_gt.mpr (hab j₁ i₂)
513 · simp [orderType, glueLT, Fin.append_right, Fin.addCases_right]
514
515end Helpers
516
517/-- Mählmann Lemma 4.15 (Bipartite Ramsey). -/
518theorem bipartiteRamsey (k ℓ₁ ℓ₂ : ℕ) (hk : 0 < k) :
519 ∃ U : ℕ → ℕ, Monotone U ∧ (∀ N : ℕ, ∃ n : ℕ, N ≤ U n) ∧
520 ∀ (n : ℕ) (c : (Fin ℓ₁ → Fin n) → (Fin ℓ₂ → Fin n) → Fin k),
521 ∃ I₁ I₂ : Finset (Fin n),
522 U n ≤ I₁.card ∧ U n ≤ I₂.card ∧
523 ∃ f : (Fin ℓ₁ × Fin ℓ₁ → Ordering) →
524 (Fin ℓ₂ × Fin ℓ₂ → Ordering) → Fin k,
525 ∀ (a : Fin ℓ₁ → Fin n) (b : Fin ℓ₂ → Fin n),
526 (∀ i, a i ∈ I₁) → (∀ j, b j ∈ I₂) →
527 c a b = f (orderType a) (orderType b) := by
528 classical
529 obtain ⟨N, hNmono, hNunb, hN⟩ := tupleRamsey k (ℓ₁ + ℓ₂) hk
530 refine ⟨fun n => N n / 2, ?_, ?_, ?_⟩
531 -- Monotonicity of `N n / 2`.
532 · intro m n hmn
533 exact Nat.div_le_div_right (hNmono hmn)
534 -- Unboundedness: given `M`, pick `n` with `N n ≥ 2M`; then
535 -- `N n / 2 ≥ M`.
536 · intro M
537 obtain ⟨n, hn⟩ := hNunb (2 * M)
538 refine ⟨n, ?_⟩
539 show M ≤ N n / 2
540 calc M = 2 * M / 2 :=
541 (Nat.mul_div_cancel_left M (by decide : (0 : ℕ) < 2)).symm
542 _ ≤ N n / 2 := Nat.div_le_div_right hn
543 · intro n c
544 -- View `c` as a coloring of `(Fin (ℓ₁ + ℓ₂) → Fin n)` tuples via
545 -- concatenation.
546 let c' : (Fin (ℓ₁ + ℓ₂) → Fin n) → Fin k := fun t =>
547 c (fun i => t (Fin.castAdd ℓ₂ i)) (fun j => t (Fin.natAdd ℓ₁ j))
548 obtain ⟨I, hIcard, f', hf'⟩ := hN n c'
549 let emb : Fin I.card ↪o Fin n := I.orderEmbOfFin rfl
550 let half : ℕ := I.card / 2
551 have hhalf_le : half ≤ I.card := Nat.div_le_self _ _
552 have hdouble_half : 2 * half ≤ I.card := Nat.mul_div_le I.card 2
553 -- `I₁` := image of `{0, …, half-1} ⊂ Fin I.card` under `emb`.
554 let I₁ : Finset (Fin n) :=
555 (Finset.univ : Finset (Fin half)).image
556 (fun i => emb ⟨i.val, lt_of_lt_of_le i.isLt hhalf_le⟩)
557 -- `I₂` := image of `{half, …, I.card-1} ⊂ Fin I.card` under `emb`.
558 let I₂ : Finset (Fin n) :=
559 (Finset.univ : Finset (Fin (I.card - half))).image
560 (fun i => emb ⟨half + i.val, by
561 have := i.isLt; omega⟩)
562 let f : (Fin ℓ₁ × Fin ℓ₁ → Ordering) →
563 (Fin ℓ₂ × Fin ℓ₂ → Ordering) → Fin k :=
564 fun ot₁ ot₂ => f' (glueLT ot₁ ot₂)
565 refine ⟨I₁, I₂, ?_, ?_, f, ?_⟩
566 -- |I₁| ≥ N n / 2.
567 · have hinj : Function.Injective
568 (fun i : Fin half =>
569 emb ⟨i.val, lt_of_lt_of_le i.isLt hhalf_le⟩) := by
570 intro i j hij
571 have h : (⟨i.val, lt_of_lt_of_le i.isLt hhalf_le⟩ : Fin I.card) =
572 ⟨j.val, lt_of_lt_of_le j.isLt hhalf_le⟩ :=
573 emb.injective hij
574 exact Fin.ext (Fin.mk_eq_mk.mp h)
575 have hcard : I₁.card = half := by
576 simp [I₁, Finset.card_image_of_injective _ hinj]
577 rw [hcard]
578 exact Nat.div_le_div_right hIcard
579 -- |I₂| ≥ N n / 2.
580 · have hinj : Function.Injective
581 (fun i : Fin (I.card - half) =>
582 emb ⟨half + i.val, by have := i.isLt; omega⟩) := by
583 intro i j hij
584 have h : (⟨half + i.val, by have := i.isLt; omega⟩ : Fin I.card) =
585 ⟨half + j.val, by have := j.isLt; omega⟩ :=
586 emb.injective hij
587 have h' : half + i.val = half + j.val := Fin.mk_eq_mk.mp h
588 exact Fin.ext (by omega)
589 have hcard : I₂.card = I.card - half := by
590 simp [I₂, Finset.card_image_of_injective _ hinj]
591 rw [hcard]
592 have h1 : N n / 2 ≤ half := Nat.div_le_div_right hIcard
593 have h2 : half ≤ I.card - half := by omega
594 exact le_trans h1 h2
595 -- Homogeneity: `c a b = f (otp a) (otp b)` for `a ∈ I₁^ℓ₁, b ∈ I₂^ℓ₂`.
596 · intro a b ha hb
597 -- Lift `a`, `b` to `Fin I.card` preimages under `emb`.
598 have hamem : ∀ i, ∃ k : Fin half,
599 emb ⟨k.val, lt_of_lt_of_le k.isLt hhalf_le⟩ = a i := by
600 intro i
601 have hm := ha i
602 simp only [I₁, Finset.mem_image, Finset.mem_univ, true_and] at hm
603 exact hm
604 have hbmem : ∀ j, ∃ k : Fin (I.card - half),
605 emb ⟨half + k.val, by have := k.isLt; omega⟩ = b j := by
606 intro j
607 have hm := hb j
608 simp only [I₂, Finset.mem_image, Finset.mem_univ, true_and] at hm
609 exact hm
610 choose ka hka using hamem
611 choose kb hkb using hbmem
612 let t : Fin (ℓ₁ + ℓ₂) → Fin n := Fin.append a b
613 -- `t i ∈ I` for every `i`.
614 have hIt : ∀ i, t i ∈ I := by
615 intro i
616 refine Fin.addCases (fun i₁ => ?_) (fun i₂ => ?_) i
617 · show (Fin.append a b) (Fin.castAdd ℓ₂ i₁) ∈ I
618 rw [Fin.append_left, ← hka i₁]
619 exact Finset.orderEmbOfFin_mem I rfl _
620 · show (Fin.append a b) (Fin.natAdd ℓ₁ i₂) ∈ I
621 rw [Fin.append_right, ← hkb i₂]
622 exact Finset.orderEmbOfFin_mem I rfl _
623 -- Every `a`-coord is strictly less than every `b`-coord.
624 have hab_lt : ∀ (i : Fin ℓ₁) (j : Fin ℓ₂), a i < b j := by
625 intro i j
626 rw [← hka i, ← hkb j]
627 apply emb.strictMono
628 simp only [Fin.mk_lt_mk]
629 have h1 : (ka i).val < half := (ka i).isLt
630 omega
631 -- Combine.
632 have htsplit : c' t = f' (orderType t) := hf' t hIt
633 have hca : c a b = c' t := by
634 show c a b = c (fun i => (Fin.append a b) (Fin.castAdd ℓ₂ i))
635 (fun j => (Fin.append a b) (Fin.natAdd ℓ₁ j))
636 simp [Fin.append_left, Fin.append_right]
637 have hot : orderType t = glueLT (orderType a) (orderType b) :=
638 orderType_append_of_lt hab_lt
639 show c a b = f' (glueLT (orderType a) (orderType b))
640 rw [hca, htsplit, hot]
641
642end Dev.MonadicDependence.BipartiteRamsey
643