Import Shelah's bound for Hales–Jewett and update density Hales–Jewett to explicit bounds

LeanPool/DensityHalesJewett.lean

@@ -7,13 +7,16 @@ Authors: Gabriel Dahia
 module
 
 public import LeanPool.DensityHalesJewett.DensityHalesJewett
+public import LeanPool.DensityHalesJewett.DensityHalesJewett.Ackermann
 public import LeanPool.DensityHalesJewett.DensityHalesJewett.Canonization
 public import LeanPool.DensityHalesJewett.DensityHalesJewett.DensityIncrement
 public import LeanPool.DensityHalesJewett.DensityHalesJewett.DensityIncrement.CorrelatedFibers
 public import LeanPool.DensityHalesJewett.DensityHalesJewett.DensityIncrement.Parameters
 public import LeanPool.DensityHalesJewett.DensityHalesJewett.DensityIncrement.StructuredCorrelation
 public import LeanPool.DensityHalesJewett.DensityHalesJewett.FiniteUnions
 public import LeanPool.DensityHalesJewett.DensityHalesJewett.GrahamRothschild
+public import LeanPool.DensityHalesJewett.DensityHalesJewett.HalesJewett
+public import LeanPool.DensityHalesJewett.DensityHalesJewett.Induction
 public import LeanPool.DensityHalesJewett.DensityHalesJewett.Insensitive
 public import LeanPool.DensityHalesJewett.DensityHalesJewett.Main
 public import LeanPool.DensityHalesJewett.DensityHalesJewett.Subspace
@@ -30,7 +33,9 @@ public import LeanPool.DensityHalesJewett.Solution
 Source: url:https://github.com/gdahia/densityhalesjewett
 Authors: Gabriel Dahia
 Status: verified
-Main declarations: `Combinatorics.Line.exists_of_density_atTop`
+Main declarations: `Combinatorics.Line.exists_of_density_atTop`,
+  `Combinatorics.Line.exists_of_density`,
+  `Combinatorics.ArithmeticProgression.exists_of_density_nat`
 Tags: combinatorics
 MSC: 05D10, 05A05, 11B75, 68R15
 -/

LeanPool/DensityHalesJewett/DensityHalesJewett.lean

@@ -5,13 +5,16 @@ Authors: Gabriel Dahia
 -/
 module
 
+public import LeanPool.DensityHalesJewett.DensityHalesJewett.Ackermann
 public import LeanPool.DensityHalesJewett.DensityHalesJewett.Canonization
 public import LeanPool.DensityHalesJewett.DensityHalesJewett.DensityIncrement
 public import LeanPool.DensityHalesJewett.DensityHalesJewett.DensityIncrement.CorrelatedFibers
 public import LeanPool.DensityHalesJewett.DensityHalesJewett.DensityIncrement.Parameters
 public import LeanPool.DensityHalesJewett.DensityHalesJewett.DensityIncrement.StructuredCorrelation
 public import LeanPool.DensityHalesJewett.DensityHalesJewett.FiniteUnions
 public import LeanPool.DensityHalesJewett.DensityHalesJewett.GrahamRothschild
+public import LeanPool.DensityHalesJewett.DensityHalesJewett.HalesJewett
+public import LeanPool.DensityHalesJewett.DensityHalesJewett.Induction
 public import LeanPool.DensityHalesJewett.DensityHalesJewett.Insensitive
 public import LeanPool.DensityHalesJewett.DensityHalesJewett.Main
 public import LeanPool.DensityHalesJewett.DensityHalesJewett.Subspace

LeanPool/DensityHalesJewett/DensityHalesJewett/Canonization.lean

@@ -6,22 +6,23 @@ Authors: Gabriel Dahia
 module
 
 public import LeanPool.DensityHalesJewett.DensityHalesJewett.Subspace
-import Mathlib.Basic.Finite.Prod
-import Mathlib.Basic.Finite.Sum
+public import LeanPool.ShelahHalesJewett.HalesJewett
+import Mathlib.Tactic.Ring.RingNF
 
 /-!
 # Canonization of the constant letters
 
 A word over the alphabet `Option α` is a word over `α` with variable positions marked by `none`;
-its support is the set of variable positions.  Substituting such a word into a combinatorial
+its support is the set of variable positions. Substituting such a word into a combinatorial
 subspace gives `Subspace.wordMap`, which turns a subspace of dimension `ℓ` into a map from words
 of length `ℓ` to words of length the ambient dimension.
 
-The main result `exists_canonical` is the support canonization lemma of
-`graham_rothschild_lines_from_mhj.tex`: after passing to a suitable `ℓ`-dimensional subspace, the
-colour of a substituted word depends only on its support.  It is proved by induction on `ℓ`, one
-application of the ordinary Hales--Jewett theorem per variable, each of them applied to the
-profile of colours obtained by letting the remaining positions vary.
+The main result `exists_canonical` is support canonization: after passing to a suitable
+`ℓ`-dimensional subspace, the colour of a substituted word depends only on its support. It is
+proved by induction on `ℓ`, one application of the ordinary Hales--Jewett theorem per variable,
+each of them applied to the profile of colours obtained by letting the remaining positions vary.
+The dimension it needs is `Canonization.bound`, an explicit expression in Shelah's bound
+`Combinatorics.Line.shelahBound` for the Hales--Jewett numbers.
 -/
 
 @[expose] public section
@@ -93,6 +94,12 @@ lemma wordMap_consLine {ℓ : ℕ} {B B' : Type*} (V : Combinatorics.Subspace (F
   | inl b => cases h : V.idxFun b <;> simp [wordMap, consLine, h]
   | inr i => cases h : l.idxFun i <;> simp [wordMap, consLine, Line.fillOption, h]
 
+lemma wordMap_reindex {ι' : Type*} (V : Combinatorics.Subspace η α ι) (e : ι ≃ ι')
+    (x : η → Option α) :
+    wordMap (V.reindex (Equiv.refl _) (Equiv.refl _) e) x = wordMap V x ∘ e.symm := by
+  funext i
+  cases h : V.idxFun (e.symm i) <;> simp [wordMap, Combinatorics.Subspace.reindex, h]
+
 /-- Embed the first `N` coordinates of a cube into a larger one, filling the remaining
 coordinates with a fixed letter. -/
 noncomputable def padInitial (α : Type*) [Nonempty α] {N n : ℕ} (h : N ≤ n) :
@@ -104,88 +111,99 @@ end Subspace
 
 namespace Canonization
 
-variable {α : Type*}
-
 open Subspace
 
+/-- The number of positions used by support canonization of `ℓ` variables over `k` letters with
+`c` colours, when `p` positions precede the block and `s` variable slots follow it. Each variable
+adds the dimension of one application of the Hales--Jewett theorem, to the colouring by profiles
+over the remaining positions. -/
+def bound (k c : ℕ) : ℕ → ℕ → ℕ → ℕ
+  | 0, _, _ => 0
+  | ℓ + 1, p, s =>
+    bound k c ℓ p (s + 1) +
+      Combinatorics.Line.shelahBound k (c ^ (k + 1) ^ (p + bound k c ℓ p (s + 1) + s))
+
 /-- The inductive form of support canonization: for any block of positions preceding the
-variables and any block of variable slots following them, there is a block of positions carrying
+variables and any block of variable slots following them, there is a block of positions with
 `ℓ` variables on which every colouring becomes a function of the support alone. -/
-private lemma exists_canonical_aux (α : Type*) [Finite α] (C : Type*) [Finite C] (ℓ : ℕ) :
-    ∀ (P S : Type) [Finite P] [Finite S], ∃ (B : Type) (_ : Finite B),
-      ∀ χ : (P → Option α) → (B → Option α) → (S → Option α) → C,
+private lemma exists_canonical_aux (α : Type*) [Fintype α] (κ : Type*) [Fintype κ] (ℓ : ℕ) :
+    ∀ (P S : Type) [Fintype P] [Fintype S], ∃ (B : Type) (_ : Fintype B),
+      Fintype.card B = bound (Fintype.card α) (Fintype.card κ) ℓ (Fintype.card P)
+        (Fintype.card S) ∧
+      ∀ C : (P → Option α) → (B → Option α) → (S → Option α) → κ,
         ∃ V : Combinatorics.Subspace (Fin ℓ) α B,
           ∀ (p : P → Option α) (s : S → Option α) (x y : Fin ℓ → Option α),
-            SameSupport x y → χ p (wordMap V x) s = χ p (wordMap V y) s := by
+            SameSupport x y → C p (wordMap V x) s = C p (wordMap V y) s := by
+  classical
   induction ℓ with
   | zero =>
     intro P S _ _
-    refine ⟨PEmpty, inferInstance, ?_⟩
-    intro χ
-    refine ⟨⟨PEmpty.elim, ?_⟩, ?_⟩
-    · intro e
-      exact e.elim0
-    · intro p s _ _ _
-      exact congrArg (fun w ↦ χ p w s) (funext fun i ↦ i.elim)
+    refine ⟨PEmpty, inferInstance, by simp [bound], ?_⟩
+    intro C
+    refine ⟨⟨PEmpty.elim, fun e ↦ e.elim0⟩, ?_⟩
+    intro p s _ _ _
+    exact congrArg (fun w ↦ C p w s) (funext fun i ↦ i.elim)
   | succ ℓ ih =>
     intro P S _ _
-    obtain ⟨B, _, hB⟩ := ih P (Unit ⊕ S)
-    obtain ⟨B', _, hB'⟩ := Combinatorics.Line.exists_mono_in_high_dimension α
-      ((P → Option α) → (B → Option α) → (S → Option α) → C)
-    refine ⟨B ⊕ B', inferInstance, ?_⟩
-    intro χ
-    obtain ⟨l, prof, hprof⟩ := hB' fun u p b s ↦ χ p (Sum.elim b (some ∘ u)) s
-    have hprof' : ∀ (a : α) (p : P → Option α) (b : B → Option α) (s : S → Option α),
-        χ p (Sum.elim b (some ∘ l a)) s = prof p b s :=
-      fun a p b s ↦ congrFun (congrFun (congrFun (hprof a) p) b) s
+    obtain ⟨B, _, hcard, hB⟩ := ih P (Unit ⊕ S)
+    rw [Fintype.card_sum, Fintype.card_unit, add_comm 1] at hcard
+    have hprofiles : Fintype.card ((P → Option α) → (B → Option α) → (S → Option α) → κ) =
+        Fintype.card κ ^ (Fintype.card α + 1) ^ (Fintype.card P + Fintype.card B +
+          Fintype.card S) := by
+      simp only [Fintype.card_fun, Fintype.card_option, ← pow_mul, ← pow_add]
+      congr 2
+      ring
+    refine ⟨B ⊕ Fin (Combinatorics.Line.shelahBound (Fintype.card α)
+      (Fintype.card ((P → Option α) → (B → Option α) → (S → Option α) → κ))),
+      inferInstance, by rw [Fintype.card_sum, Fintype.card_fin, hprofiles, hcard, bound], ?_⟩
+    intro C
+    -- A line on the new block along which the colouring of the other positions is constant.
+    obtain ⟨l, profile, hl⟩ := Combinatorics.Line.exists_mono_of_card_eq_shelahBound
+      (Fintype.card_fin _) fun (u : _ → α) p b s ↦ C p (Sum.elim b (some ∘ u)) s
+    have hprofile (a : α) (p : P → Option α) (b : B → Option α) (s : S → Option α) :
+        C p (Sum.elim b (some ∘ l a)) s = profile p b s :=
+      congrFun (congrFun (congrFun (hl a) p) b) s
+    -- Canonize the earlier variables, with the new one among the slots that follow them.
     obtain ⟨V, hV⟩ := hB fun p b q ↦
-      χ p (Sum.elim b (Line.fillOption l (q (Sum.inl ())))) fun s ↦ q (Sum.inr s)
+      C p (Sum.elim b (Line.fillOption l (q (Sum.inl ())))) fun s ↦ q (Sum.inr s)
     refine ⟨consLine V l, ?_⟩
     intro p s x y hxy
     rw [wordMap_consLine, wordMap_consLine]
-    apply Eq.trans (hV p (Sum.elim (fun _ ↦ x 0) s) (fun i ↦ x i.succ) (fun i ↦ y i.succ)
-      fun i ↦ hxy i.succ)
+    refine (hV p (Sum.elim (fun _ ↦ x 0) s) (fun i ↦ x i.succ) (fun i ↦ y i.succ)
+      fun i ↦ hxy i.succ).trans ?_
     simp only [Sum.elim_inl, Sum.elim_inr]
     cases hx : x 0 with
     | none => rw [(hxy 0).1 hx]
     | some a =>
       cases hy : y 0 with
       | none => simp [(hxy 0).2 hy] at hx
-      | some b =>
-        rw [Line.fillOption_some, Line.fillOption_some, hprof' a, hprof' b]
+      | some b => rw [Line.fillOption_some, Line.fillOption_some, hprofile a, hprofile b]
+
+variable {α κ : Type*} [Fintype α] [Fintype κ] {ℓ : ℕ}
 
 /-- **Support canonization**: in a large enough cube every colouring of words over `Option α`
 admits an `ℓ`-dimensional subspace on which the colour of a substituted word depends only on its
 support. -/
-lemma exists_canonical (α : Type*) [Finite α] (C : Type*) [Finite C] (ℓ : ℕ) :
-    ∃ N : ℕ, ∀ χ : (Fin N → Option α) → C,
-      ∃ V : Combinatorics.Subspace (Fin ℓ) α (Fin N),
-        ∀ x y : Fin ℓ → Option α, SameSupport x y → χ (wordMap V x) = χ (wordMap V y) := by
-  obtain ⟨B, _, hB⟩ := exists_canonical_aux α C ℓ PEmpty PEmpty
-  have := Fintype.ofFinite B
-  refine ⟨Fintype.card B, ?_⟩
-  intro χ
-  obtain ⟨V, hV⟩ := hB fun _ w _ ↦ χ (w ∘ (Fintype.equivFin B).symm)
-  have hw (z : Fin ℓ → Option α) :
-      wordMap (V.reindex (Equiv.refl _) (Equiv.refl _) (Fintype.equivFin B)) z
-        = wordMap V z ∘ (Fintype.equivFin B).symm := by
-    funext i
-    cases h : V.idxFun ((Fintype.equivFin B).symm i) <;>
-      simp [wordMap, Combinatorics.Subspace.reindex, h]
-  refine ⟨V.reindex (Equiv.refl _) (Equiv.refl _) (Fintype.equivFin B), ?_⟩
+lemma exists_canonical
+    (C : (Fin (bound (Fintype.card α) (Fintype.card κ) ℓ 0 0) → Option α) → κ) :
+    ∃ V : Combinatorics.Subspace (Fin ℓ) α
+        (Fin (bound (Fintype.card α) (Fintype.card κ) ℓ 0 0)),
+      ∀ x y : Fin ℓ → Option α, SameSupport x y → C (wordMap V x) = C (wordMap V y) := by
+  obtain ⟨B, _, hcard, hB⟩ := exists_canonical_aux α κ ℓ PEmpty PEmpty
+  rw [Fintype.card_pempty] at hcard
+  let e := Fintype.equivFinOfCardEq hcard
+  obtain ⟨V, hV⟩ := hB fun _ w _ ↦ C (w ∘ e.symm)
+  refine ⟨V.reindex (Equiv.refl _) (Equiv.refl _) e, ?_⟩
   intro x y hxy
-  rw [hw x, hw y]
+  rw [wordMap_reindex, wordMap_reindex]
   exact hV PEmpty.elim PEmpty.elim x y hxy
 
 /-- Support canonization holds in every ambient dimension beyond the one it produces. -/
-lemma exists_canonical_of_le (α : Type*) [Finite α] [Nonempty α] (C : Type*) [Finite C] (ℓ : ℕ) :
-    ∃ N : ℕ, ∀ n, N ≤ n → ∀ χ : (Fin n → Option α) → C,
-      ∃ V : Combinatorics.Subspace (Fin ℓ) α (Fin n),
-        ∀ x y : Fin ℓ → Option α, SameSupport x y → χ (wordMap V x) = χ (wordMap V y) := by
-  obtain ⟨N, hN⟩ := exists_canonical α C ℓ
-  refine ⟨N, ?_⟩
-  intro n hn χ
-  obtain ⟨V, hV⟩ := hN fun w ↦ χ (wordMap (padInitial α hn) w)
+lemma exists_canonical_of_le [Nonempty α] {n : ℕ}
+    (hn : bound (Fintype.card α) (Fintype.card κ) ℓ 0 0 ≤ n) (C : (Fin n → Option α) → κ) :
+    ∃ V : Combinatorics.Subspace (Fin ℓ) α (Fin n),
+      ∀ x y : Fin ℓ → Option α, SameSupport x y → C (wordMap V x) = C (wordMap V y) := by
+  obtain ⟨V, hV⟩ := exists_canonical fun w ↦ C (wordMap (padInitial α hn) w)
   refine ⟨compose (padInitial α hn) V, ?_⟩
   intro x y hxy
   rw [wordMap_compose, wordMap_compose]