UpperBound.lean`

26 declarations, 0 contain sorry, 0 declared as axioms

def OAI.QuantitativeVanDerWaerden.focusSize line 12

Source documentation

The inner recursion, with the bound for the preceding length supplied.

def focusSize (previous : ℕ → ℕ) (r : ℕ) : ℕ → ℕ
  | 0 => 1
  | t + 1 => 2 * focusSize previous r t * previous (r ^ focusSize previous r t)

/-- Length is the recursion argument; all color counts at the previous
length are available before the next length is constructed. -/

def OAI.QuantitativeVanDerWaerden.Fcore line 18
Source documentation
Length is the recursion argument; all color counts at the previous length are available before the next length is constructed.
```
def Fcore : ℕ → ℕ → ℕ
  | 0, _ => 1
  | 1, _ => 1
  | 2, r => r + 1
  | k + 3, r => focusSize (Fcore (k + 2)) r r
```
Mentions: OAI.QuantitativeVanDerWaerden.focusSize
def OAI.QuantitativeVanDerWaerden.F line 24
theorem OAI.QuantitativeVanDerWaerden.F_one line 26
theorem OAI.QuantitativeVanDerWaerden.F_two line 27
theorem OAI.QuantitativeVanDerWaerden.F_recursion line 28
theorem OAI.QuantitativeVanDerWaerden.focusSize_pos line 31
theorem OAI.QuantitativeVanDerWaerden.Fcore_pos line 39
theorem OAI.QuantitativeVanDerWaerden.F_pos line 49
theorem OAI.QuantitativeVanDerWaerden.hasMonoAP_two_of_lt line 51
theorem OAI.QuantitativeVanDerWaerden.isRamsey_two line 60
structure OAI.QuantitativeVanDerWaerden.Focus line 73
Source documentation
A focus with distinct arm colors. The arms have length k - 1, and adding their common next point would give a progression of length k.
```
structure Focus {α : Type uAlpha} (c : ℕ → α) (k N t : ℕ) where
…
```
theorem OAI.QuantitativeVanDerWaerden.Focus.color_ne line 83
theorem OAI.QuantitativeVanDerWaerden.fin_cases_injective line 97
theorem OAI.QuantitativeVanDerWaerden.Focus.impossible line 111
def OAI.QuantitativeVanDerWaerden.blockWord line 119
theorem OAI.QuantitativeVanDerWaerden.matching_point line 122
theorem OAI.QuantitativeVanDerWaerden.next_block_lt line 128
Source documentation
The next block is allocated, even though its word need not match.
```
private theorem next_block_lt {k b d B : ℕ} (hk : 3 ≤ k)
    (hb : b + (k - 2) * d < B) : b + (k - 1) * d < 2 * B := by
…
```
theorem OAI.QuantitativeVanDerWaerden.focus_lift line 138
Source documentation
Copy the old arms into matching blocks and add the arm supplied by the old focus. All positions and differences are kept explicitly.
```
theorem focus_lift {α : Type uAlpha} {c : ℕ → α} {k m B b d t : ℕ}
    (hk : 3 ≤ k) (hm : 0 < m) (hd : 0 < d)
    (hb : b + (k - 2) * d < B)
    (hw : MonoAP (blockWord c m) (k - 1) b d)
    (old : Focus (fun x => c (b * m + x)) k m t)
    (ha : ¬ HasMonoAP (fun x => c (b * m + x)) k m) :
    Nonempty (Focus c k (2 * m * B) (t + 1)) := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.MonoAP, OAI.QuantitativeVanDerWaerden.blockWord, OAI.QuantitativeVanDerWaerden.Focus, OAI.QuantitativeVanDerWaerden.HasMonoAP

theorem OAI.QuantitativeVanDerWaerden.focusing line 204

Source documentation

The inner focusing induction, simultaneously for every finite color type so that complete block words can themselves serve as colors.

theorem focusing {α : Type u} [Fintype α] {previous : ℕ → ℕ} {k : ℕ}
    (hk : 3 ≤ k) (hr : 0 < Fintype.card α)
    (hp : ∀ r, 0 < r → 0 < previous r)
    (hprevious : ∀ (β : Type u) [Fintype β], 0 < Fintype.card β →
      IsRamsey β (k - 1) (previous (Fintype.card β))) :
    ∀ (t : ℕ) (c : ℕ → α),
      ¬ HasMonoAP c k (focusSize previous (Fintype.card α) t) →
      Nonempty (Focus c k (focusSize previous (Fintype.card α) t) t) := by
…

Mentions: OAI.QuantitativeVanDerWaerden.IsRamsey, OAI.QuantitativeVanDerWaerden.HasMonoAP, OAI.QuantitativeVanDerWaerden.focusSize, OAI.QuantitativeVanDerWaerden.Focus

theorem OAI.QuantitativeVanDerWaerden.isRamsey_Fcore line 252
theorem OAI.QuantitativeVanDerWaerden.isRamsey_F line 272
theorem OAI.QuantitativeVanDerWaerden.finite_ramsey line 277
Source documentation
Unconditional finiteness for every positive color count and length.
```
theorem finite_ramsey {r k : ℕ} (hr : 0 < r) (hk : 0 < k) :
    ∃ N, 0 < N ∧ IsRamsey (Fin r) k N := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.IsRamsey
theorem OAI.QuantitativeVanDerWaerden.W_le_F line 282
theorem OAI.QuantitativeVanDerWaerden.W_spec line 286
theorem OAI.QuantitativeVanDerWaerden.W_two line 289