English
For all n in N, (n/3 − 2) · rothNumberNat((n−3)/6) ≤ ruzsaSzemerediNumberNat n.
Русский
Для всех n ∈ ℕ: (n/3 − 2) · rothNumberNat((n−3)/6) ≤ ruzsaSzemerediNumberNat n.
LaTeX
$$$ \\left(\\frac{n}{3} - 2\\right) \\cdot \\operatorname{rothNumberNat}\\left(\\frac{n - 3}{6}\\right) \\le \\operatorname{ruzsaSzemerediNumberNat}(n) $$$
Lean4
/-- Lower bound on the **Ruzsa-Szemerédi problem** in terms of 3AP-free sets.
If there exists a 3AP-free subset of `[1, ..., (n - 3) / 6]` of size `m`, then there exists a graph
with `n` vertices and `(n / 3 - 2) * m` edges such that each edge belongs to exactly one triangle.
-/
theorem rothNumberNat_le_ruzsaSzemerediNumberNat' :
∀ n : ℕ, (n / 3 - 2 : ℝ) * rothNumberNat ((n - 3) / 6) ≤ ruzsaSzemerediNumberNat n
| 0 => by simp
| 1 => by simp
| 2 => by simp
| n + 3 =>
by
calc
_ ≤ (↑(2 * (n / 6) + 1) : ℝ) * rothNumberNat (n / 6) := mul_le_mul_of_nonneg_right ?_ (Nat.cast_nonneg _)
_ ≤ (ruzsaSzemerediNumberNat (6 * (n / 6) + 3) : ℝ) := ?_
_ ≤ _ := Nat.cast_le.2 (ruzsaSzemerediNumberNat_mono <| add_le_add_right (Nat.mul_div_le _ _) _)
· norm_num
rw [← div_add_one (three_ne_zero' ℝ), ← le_sub_iff_add_le, div_le_iff₀ (zero_lt_three' ℝ), add_assoc,
add_sub_assoc, add_mul, mul_right_comm]
norm_num
norm_cast
rw [← mul_add_one]
exact (Nat.lt_mul_div_succ _ <| by simp).le
· norm_cast
exact rothNumberNat_le_ruzsaSzemerediNumberNat _
