Colourings with only short monochromatic progressions

DefinitionStatement of Erdős Problem 984 on short monochromatic progressions#✓fully proved

The proposition that there is a colouring of the positive integers with two colours such that for every real \(\varepsilon > 0\) there is a real constant \(C_\varepsilon\) with the following property: whenever \(a \ge 1\), \(d \ge 1\) and \(k \ge 0\) are integers and \(a, a + d, \dots, a + (k - 1)d\) all have the same colour, \(k \le C_\varepsilon a^\varepsilon\).

def twoColouringShortProgressions : Prop :=
  ∃ c : ℕ → Fin 2, ∀ ε : ℝ, 0 < ε → ∃ C : ℝ, ∀ a d k : ℕ, 1 ≤ a → 1 ≤ d →
    (∀ i < k, c (a + i * d) = c a) → (k : ℝ) ≤ C * (a : ℝ) ^ ε

Used by 1

Used byErdős Problem 984: a two-colouring with short monochromatic progressions exists

TheoremErdős Problem 984: a two-colouring with short monochromatic progressions exists#●ready to prove

There is a colouring of the positive integers with two colours such that for every real \(\varepsilon > 0\) there is a real constant \(C_\varepsilon\) with the following property: whenever \(a \ge 1\), \(d \ge 1\) and \(k \ge 0\) are integers and \(a, a + d, \dots, a + (k - 1)d\) all have the same colour, \(k \le C_\varepsilon a^\varepsilon\).

public theorem_wanted twoColouringShortProgressions_holds : twoColouringShortProgressions

Sources

• T. F. Bloom, Erdős Problems, Problem #984, https://www.erdosproblems.com/984 (status PROVED); resolution: Z. Hunter, proof in the erdosproblems.com/984 comments, using Green's red-blue colourings for off-diagonal van der Waerden numbers, erdosproblems.com/984: 'Zach Hunter has proved the answer is yes (see the comments)'; the comment colours each block I_t = [100^t, 100^{t+1}) with no red 3-term progression and no blue progression of length k_t = |I_t|^{o(1)} for odd t (colours swapped for even t), https://www.erdosproblems.com/forum/thread/984.

Uses 1

Statement usesStatement of Erdős Problem 984 on short monochromatic progressions

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.