Theorems · Definition · number theory

rothNumberNat

ℕ →o ℕ

The Roth number of a natural N is the largest integer m for which there is a subset of range N of size m with no arithmetic progression of length 3. Trivially, rothNumberNat N ≤ N, but Roth's theorem (proved in 1953) shows that rothNumberNat N = o(N) and the construction by Behrend gives a lower bound of the form N * exp(-C sqrt(log(N))) ≤ rothNumberNat N. A significant refinement of Roth's theorem by Bloom and Sisask announced in 2020 gives rothNumberNat N = O(N / (log N)^(1+c)) for an absolute constant c.

Defined in

Mathlib.Combinatorics.Additive.AP.Three.Defs

Cited by

17 results in Mathlib

Foundations

Depth 74 from the axioms · uses propext, Classical.choice, Quot.sound