English
Roth’s theorem for ℕ: the maximum density of a 3AP-free subset of {1,...,n} is o(1) as n → ∞; more precisely, for ε>0 and n large enough, any A ⊆ {1,...,n} with density at least εn contains a 3-term progression.
Русский
Теорема Рота для натуральных чисел: максимальная плотность множества без 3-терминной арифметической прогрессии внутри {1,...,n} стремится к нулю по мере роста n; для больших n любая подмножество с плотностью не менее εn содержит 3-терминную прогрессию.
LaTeX
$$$\forall \varepsilon>0,\ h_{\varepsilon}: 0<\varepsilon,\ h_G: cornersTheoremBound(\varepsilon/3) \le n,\ A \subseteq \mathbb{N},\ h_{A\varepsilon}: \varepsilon \cdot n \le |A| \Rightarrow \neg ThreeAPFree(A).$$$
Lean4
/-- **Roth's theorem** for `ℕ`.
The maximum density of a 3AP-free set in `{1, ..., n}` goes to zero as `n` tends to infinity. -/
theorem roth_3ap_theorem_nat (ε : ℝ) (hε : 0 < ε) (hG : cornersTheoremBound (ε / 3) ≤ n) (A : Finset ℕ)
(hAn : A ⊆ range n) (hAε : ε * n ≤ #A) : ¬ThreeAPFree (A : Set ℕ) :=
by
rintro hA
rw [← coe_subset, coe_range] at hAn
have : A = Fin.val '' (Nat.cast '' A : Set (Fin (2 * n).succ)) :=
by
rw [Set.image_image, Set.image_congr, Set.image_id]
simp only [mem_coe, Nat.succ_eq_add_one, Fin.val_natCast, id_eq, Nat.mod_succ_eq_iff_lt]
rintro a ha
have := hAn ha
simp at this
omega
rw [this] at hA
have := Fin.isAddFreimanIso_Iio two_ne_zero (le_refl (2 * n))
have :=
hA.of_image this.isAddFreimanHom Fin.val_injective.injOn <|
Set.image_subset_iff.2 <|
hAn.trans fun x hx ↦ Fin.natCast_strictMono (by cutsat) <| by simpa only [coe_range, Set.mem_Iio] using hx
rw [← coe_image] at this
refine roth_3ap_theorem (ε / 3) (by positivity) (by simp; cutsat) _ ?_ this
calc
_ = ε / 3 * (2 * n + 1) := by simp
_ ≤ ε / 3 * (2 * n + n) := by gcongr; simp; unfold cornersTheoremBound at hG; cutsat
_ = ε * n := by ring
_ ≤ #A := hAε
_ = _ := by
rw [card_image_of_injOn]
exact (CharP.natCast_injOn_Iio (Fin (2 * n).succ) (2 * n).succ).mono <| hAn.trans <| by simp; cutsat
