Basic.lean`

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.QuantitativeVanDerWaerden.apTerm_lt line 9
theorem OAI.QuantitativeVanDerWaerden.apStart_lt line 15
theorem OAI.QuantitativeVanDerWaerden.MonoAP.recolor line 18
theorem OAI.QuantitativeVanDerWaerden.MonoAP.of_injective_recolor line 23
theorem OAI.QuantitativeVanDerWaerden.HasMonoAP.recolor line 29
theorem OAI.QuantitativeVanDerWaerden.HasMonoAP.of_injective_recolor line 34
theorem OAI.QuantitativeVanDerWaerden.not_hasMonoAP_of_recolor_injective line 40
theorem OAI.QuantitativeVanDerWaerden.HasMonoAP.mono line 45
theorem OAI.QuantitativeVanDerWaerden.HasMonoAP.mono_length line 50
theorem OAI.QuantitativeVanDerWaerden.HasMonoAP.length_le line 59
theorem OAI.QuantitativeVanDerWaerden.HasMonoAP.congr line 66
theorem OAI.QuantitativeVanDerWaerden.HasMonoAP.translate line 75
theorem OAI.QuantitativeVanDerWaerden.IsRamsey.mono line 83
theorem OAI.QuantitativeVanDerWaerden.IsRamsey.of_injective line 87
theorem OAI.QuantitativeVanDerWaerden.isRamsey_one line 93
theorem OAI.QuantitativeVanDerWaerden.isRamsey_subsingleton line 100
def OAI.QuantitativeVanDerWaerden.FiniteHasMonoAP line 107
Source documentation
A literal finite-coloring formulation of the same progression.
```
def FiniteHasMonoAP {α : Type uAlpha} {N : ℕ} (c : Fin N → α) (k : ℕ) : Prop :=
…
```
def OAI.QuantitativeVanDerWaerden.restrictColor line 113
theorem OAI.QuantitativeVanDerWaerden.hasMonoAP_iff_finite_restriction line 116
theorem OAI.QuantitativeVanDerWaerden.isRamsey_iff_finite line 126
Source documentation
Only the finitely many colors on [0,N) matter. The nonempty color type allows every finite coloring to be extended beyond that interval.
```
theorem isRamsey_iff_finite (α : Type uAlpha) [Nonempty α] (k N : ℕ) :
    IsRamsey α k N ↔ ∀ c : Fin N → α, FiniteHasMonoAP c k := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.IsRamsey, OAI.QuantitativeVanDerWaerden.FiniteHasMonoAP
theorem OAI.QuantitativeVanDerWaerden.W_le_of_isRamsey line 141
theorem OAI.QuantitativeVanDerWaerden.W_spec_of_finite line 145
theorem OAI.QuantitativeVanDerWaerden.lt_W_of_avoiding line 152
Source documentation
An avoiding coloring gives a strict lower bound once finiteness has been proved. Monotonicity is used: failure at one size alone is not minimality.
```
theorem lt_W_of_avoiding {r k N : ℕ}
    (hfinite : ∃ M, 0 < M ∧ IsRamsey (Fin r) k M)
    (c : ℕ → Fin r) (hc : ¬ HasMonoAP c k N) : N < W r k := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.IsRamsey, OAI.QuantitativeVanDerWaerden.HasMonoAP
theorem OAI.QuantitativeVanDerWaerden.lt_W_of_not_isRamsey line 159
theorem OAI.QuantitativeVanDerWaerden.W_one line 166
theorem OAI.QuantitativeVanDerWaerden.W_one_color line 171