English
For every natural number n, there exists a graph on n vertices in which every edge lies in exactly one triangle, and the number of edges is at least (n/3 − 2)·((n − 3)/6)·exp(−4√log((n − 3)/6)).
Русский
Пусть n — натуральное число. Существует граф на n вершинах, в котором каждое ребро принадлежит ровно одному треугольнику, и число ребер не меньше (n/3 − 2)·((n − 3)/6)·exp(−4√log((n − 3)/6)).
LaTeX
$$$\\left(\\dfrac{n}{3}-2\\right)\\left(\\dfrac{n-3}{6}\\right)\\exp\\left(-4\\sqrt{\\log\\left(\\dfrac{n-3}{6}\\right)}\\right) \\le \\mathrm{ruzsaSzemerediNumberNat}(n).$$$
Lean4
/-- Explicit lower bound on the **Ruzsa-Szemerédi problem**.
There exists a graph with `n` vertices and
`(n / 3 - 2) * (n - 3) / 6 * exp (-4 * √(log ((n - 3) / 6)))` edges such that each edge belongs
to exactly one triangle. -/
theorem ruzsaSzemerediNumberNat_lower_bound (n : ℕ) :
(n / 3 - 2 : ℝ) * ↑((n - 3) / 6) * exp (-4 * √(log ↑((n - 3) / 6))) ≤ ruzsaSzemerediNumberNat n :=
by
rw [mul_assoc]
obtain hn | hn := le_total (n / 3 - 2 : ℝ) 0
· exact (mul_nonpos_of_nonpos_of_nonneg hn <| by positivity).trans (Nat.cast_nonneg _)
exact (mul_le_mul_of_nonneg_left Behrend.roth_lower_bound hn).trans (rothNumberNat_le_ruzsaSzemerediNumberNat' _)
