Van der Waerden-type theorems

Monochromatic arithmetic progressions: van der Waerden's theorem and van der Waerden numbers (off-diagonal, W(3,k)), short or large-difference progressions, rainbow progressions, descending waves, accessible sets and diffsequences, and progression-free Ramsey sets.

• Accessible sets and diffsequences
• Colourings with only short monochromatic progressions
• Monochromatic descending waves
• Monochromatic or rainbow arithmetic progressions
• Monochromatic progressions with large common difference
• Progression-free Ramsey sets
• Van der Waerden numbers W(3, k)
• Zero-sum van der Waerden theorems for symmetric functions

TheoremVan der Waerden's theorem#✓fully proved

For all positive integers \(r\) and \(k\) there is a natural number \(N\) such that for every coloring of \(\{1, \dots, N\}\) with \(r\) colors there are natural numbers \(a \ge 1\) and \(d \ge 1\) with \(a + (k - 1)d \le N\) such that each of the \(k\) terms \(a, a + d, \dots, a + (k - 1)d\) has the same color as \(a\).

Proof: apply the Hales–Jewett theorem to the digit-sum encoding \(x \mapsto 1 + \sum_i x_i\) of words over the alphabet \(\{0, \dots, k - 1\}\), so that a combinatorial line becomes an arithmetic progression. This follows the standard derivation in Graham, Rothschild, and Spencer, Ramsey Theory, Section 2.3, from van der Waerden (1927).

theorem vanDerWaerden : ∀ (r k : Nat), 0 < r → 0 < k →
    ∃ N : Nat, ∀ c : {m : Nat // 1 ≤ m ∧ m ≤ N} → Fin r, ∃ a d : Nat,
      1 ≤ a ∧ 1 ≤ d ∧ a + (k - 1) * d ≤ N ∧
        ∀ i : Nat, i < k → ∀ (h₁ : 1 ≤ a + i * d) (h₂ : a + i * d ≤ N)
          (h₀ : 1 ≤ a ∧ a ≤ N), c ⟨a + i * d, h₁, h₂⟩ = c ⟨a, h₀⟩

Sources

• https://en.wikipedia.org/wiki/Van_der_Waerden%27s_theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.