English
Let N be a natural number. The Roth number rothNumberNat(N) is the maximal size of a subset of {0,1,...,N−1} that contains no three-term arithmetic progression.
Русский
Пусть N — натуральное число. Число Рота rothNumberNat(N) есть максимальная мощность подмножества A ⊆ {0,1, ..., N−1}, такого, что A не содержит арифметическую прогрессию длины 3.
LaTeX
$$$\\operatorname{rothNumberNat}(N) = \\max\\{ |A| : A \\subseteq \\{0,1,\\dots,N-1\\},\\ ThreeAPFree(A) \\}.$$$
Lean4
/-- 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`. -/
def rothNumberNat : ℕ →o ℕ :=
⟨fun n => addRothNumber (range n), addRothNumber.mono.comp range_mono⟩
