Erdős Problem 138

References:

• erdosproblems.com/138
• [Be68] Berlekamp, E. R., A construction for partitions which avoid long arithmetic progressions. Canad. Math. Bull. (1968), 409-414.
• [Er80] Erdős, Paul, A survey of problems in combinatorial number theory. Ann. Discrete Math. (1980), 89-115.
• [Er81] Erdős, P., On the combinatorial problems which I would most like to see solved. Combinatorica (1981), 25-42.
• [Go01] Gowers, W. T., A new proof of Szemerédi's theorem. Geom. Funct. Anal. (2001), 465-588.

def Erdos138.monoAP_guarantee_set (r k : ℕ) : Set ℕ

The set of natural numbers that guarantee a monochromatic arithmetic progression.

A number N belongs to this set if, for a given number of colors r and an arithmetic progression length k, any r-coloring of the integers {1, ..., N} must contain a monochromatic arithmetic progression of length k.

Equations

• Erdos138.monoAP_guarantee_set r k = {N : ℕ | ∀ (coloring : { x : ℕ // x ∈ Finset.Icc 1 N } → Fin r), ContainsMonoAPofLength coloring k}

theorem Erdos138.monoAP_guarantee_set_nonempty (r k : ℕ) : (monoAP_guarantee_set r k).Nonempty

Asserts that for any number of colors r and any progression length k, there always exists some number N large enough to guarantee a monochromatic arithmetic progression. In other words, the set monoAP_guarantee_set is non-empty. This is the fundamental existence result that allows for the definition of the van der Waerden numbers.

noncomputable def Erdos138.monoAPNumber (r k : ℕ) : ℕ

The van der Waerden number, is the smallest integer N such that any r-coloring of {1, ..., N} is guaranteed to contain a monochromatic arithmetic progression of length k. It is defined as the infimum of the (non-empty) set of all such numbers N.

Equations

• Erdos138.monoAPNumber r k = sInf (Erdos138.monoAP_guarantee_set r k)

@[reducible, inline]

noncomputable abbrev Erdos138.W : ℕ → ℕ

An abbreviation for the van der Waerden number for 2 colors, commonly written as W(k). This represents the smallest integer N such that any 2-coloring of {1, ..., N} must contain a monochromatic arithmetic progression of length k.

Equations

• Erdos138.W = Erdos138.monoAPNumber 2

theorem Erdos138.monoAPNumber_two_one : W 1 = 1

theorem Erdos138.monoAPNumber_two_two : W 2 = 3

theorem Erdos138.erdos_138 : Filter.Tendsto (fun (k : ℕ) => ↑(W k) ^ (1 / ↑k)) Filter.atTop Filter.atTop ↔ sorry

In [Er80] Erdős asks whether $$ \lim_{k \to \infty} (W(k))^{1/k} = \infty $$

theorem Erdos138.erdos_138.variants.prime (p : ℕ) (hp : Nat.Prime p) : p ^ 2 ^ p ≤ W (p + 1)

When $p$ is prime Berlekamp [Be68] has proved $W(p+1) ≥ p^{2^p}$.

theorem Erdos138.erdos_138.variants.upper (k : ℕ) : W k ≤ 2 ^ 2 ^ 2 ^ 2 ^ 2 ^ (k + 9)

Gowers [Go01] has proved $$W(k) \leq 2^{2^{2^{2^{2^{k+9}}}}.$$

theorem Erdos138.erdos_138.variants.quotient : Filter.Tendsto (fun (k : ℕ) => ↑(W (k + 1)) / ↑(W k)) Filter.atTop Filter.atTop ↔ sorry

In [Er81] Erdős asks whether $\frac{W(k+1)}{W(k)} \to \infty$.

theorem Erdos138.erdos_138.variants.difference : Filter.Tendsto (fun (k : ℕ) => W (k + 1) - W k) Filter.atTop Filter.atTop ↔ sorry

In [Er81] Erdős asks whether $W(k+1) - W(k) \to \infty$.

theorem Erdos138.erdos_138.variants.dvd_two_pow : Filter.Tendsto (fun (k : ℕ) => ↑(W k) / 2 ^ k) Filter.atTop Filter.atTop ↔ sorry

In [Er80] Erdős asks whether $W(k)/2^k\to \infty$.