English
Let n be a natural number. Then (2n+1) times the Roth number at n is at most the Ruzsa–Szemerédi number at 6n+3.
Русский
Пусть n — натуральное число. Тогда (2n+1) · rothNumberNat(n) ≤ ruzsaSzemerediNumberNat(6n+3).
LaTeX
$$$ (2 \\cdot n + 1) \\cdot \\operatorname{rothNumberNat}(n) \\le \\operatorname{ruzsaSzemerediNumberNat}(6 \\cdot n + 3) $$$
Lean4
theorem rothNumberNat_le_ruzsaSzemerediNumberNat (n : ℕ) :
(2 * n + 1) * rothNumberNat n ≤ ruzsaSzemerediNumberNat (6 * n + 3) :=
by
let α := Fin (2 * n + 1)
have : Nat.Coprime 2 (2 * n + 1) := by simp
haveI : Fact (IsUnit (2 : Fin (2 * n + 1))) := ⟨by simpa using (ZMod.unitOfCoprime 2 this).isUnit⟩
open scoped Fin.CommRing in
calc
(2 * n + 1) * rothNumberNat n
_ = Fintype.card α * addRothNumber (Iio (n : α)) := by
rw [Fin.addRothNumber_eq_rothNumberNat le_rfl, Fintype.card_fin]
_ ≤ Fintype.card α * addRothNumber (univ : Finset α) := by gcongr; exact subset_univ _
_ ≤ ruzsaSzemerediNumber (Sum α (Sum α α)) := (addRothNumber_le_ruzsaSzemerediNumber _)
_ = ruzsaSzemerediNumberNat (6 * n + 3) :=
by
simp_rw [← ruzsaSzemerediNumberNat_card, Fintype.card_sum, α, Fintype.card_fin]
ring_nf
