Schur and Rado theorems

Monochromatic solutions of equations: Schur's theorem and Schur and modular Schur numbers, Rado's theorem and disjunctive Rado, monochromatic linear equations, monochromatic sums, sums of squares and products, and rainbow-free colourings of x−y=z^k.

• Modular Schur numbers
• Monochromatic solutions of linear equations
• Monochromatic sums
• Monochromatic sums equal to perfect powers
• Monochromatic sums of products
• Rainbow-free colorings for x − y = z^k
• Schur numbers

TheoremBounded representations with one scaled part#●ready to prove

Let \(a\), \(\lambda\), \(n\) and \(N\) be natural numbers with \(a \ge 3\), \(n \ge 1\), \(\lambda \ge a - 1\) and \(N \le \lambda (a + n)\). Then there are natural numbers \(x_0, \dots, x_{n-1}\) and \(y\), each at most \(\lambda\), such that \(x_0 + \dots + x_{n-1} + a y = N\).

The endpoint \(N = 0\) is included as in the paper's displayed range \(\{0, \dots, \lambda(a + n)\}\); that case is trivial, all parts being \(0\).

theorem_wanted exists_bounded_rep (a lam n N : ℕ)
    (ha : 3 ≤ a) (hn : 1 ≤ n) (hlam : a - 1 ≤ lam)
    (hN : N ≤ lam * (a + n)) :
    ∃ (x : ℕ → ℕ) (y : ℕ),
      (∀ i : ℕ, i < n → x i ≤ lam) ∧ y ≤ lam ∧
        (∑ i ∈ Finset.range n, x i) + a * y = N

Sources

• Srashti Dwivedi and Amitabha Tripathi, "On the Two-Color Disjunctive Rado Number for the Equations ∑_{i=1}^{m-2} x_i + a x_{m-1} - x_m = c_j, j = 1, 2", Proposition 4.

TheoremSchur's theorem#✓fully proved

For every integer \(r \ge 1\) there is a natural number \(S\) such that for every coloring of the natural numbers with \(r\) colors there are \(x, y, z \in \{1, \dots, S\}\), not necessarily distinct, with the same color and \(x + y = z\).

The bound comes from Ramsey's theorem for pairs, by coloring each pair with the color of its difference; it is not the Schur number \(S(r)\), the largest \(S\) for which some \(r\)-coloring of \(\{1, \dots, S\}\) has no such solution.

theorem schur_ramsey : ∀ r : ℕ, 1 ≤ r →
    ∃ S : ℕ, ∀ c : ℕ → Fin r, ∃ x y z : ℕ,
      x ∈ Finset.Icc 1 S ∧ y ∈ Finset.Icc 1 S ∧ z ∈ Finset.Icc 1 S ∧
        c x = c y ∧ c x = c z ∧ x + y = z

Sources

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

Uses 1

Proof usesFinite Ramsey theorem for pairs

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.