English
As n grows, the Ruzsa-Szemerédi number RS(n) eventually dominates n^2·e^(−4√log n) up to a constant factor; i.e., RS(n) is at least on the order of n^2·e^(−4√log n).
Русский
С ростом n число Рузса–Szemerédi RS(n) растет как минимум как константное множитель от n^2·e^(−4√log n).
LaTeX
$$$n^2 \\exp(-4\\sqrt{\\log n}) = O(\\mathrm{ruzsaSzemerediNumberNat}(n)) \\quad (n \\to \\infty).$$$
Lean4
/-- Asymptotic lower bound on the **Ruzsa-Szemerédi problem**.
There exists a graph with `n` vertices and `Ω((n ^ 2 * exp (-4 * √(log n))))` edges such that
each edge belongs to exactly one triangle. -/
theorem ruzsaSzemerediNumberNat_asymptotic_lower_bound :
(fun n ↦ n ^ 2 * exp (-4 * √(log n)) : ℕ → ℝ) =O[atTop] fun n ↦ (ruzsaSzemerediNumberNat n : ℝ) :=
by
trans fun n ↦ (n / 3 - 2) * ↑((n - 3) / 6) * exp (-4 * √(log ↑((n - 3) / 6)))
· simp_rw [sq]
refine (IsBigO.mul ?_ ?_).mul ?_
· trans fun n ↦ n / 3
· simp_rw [div_eq_inv_mul]
exact (isBigO_refl ..).const_mul_right (by simp)
refine IsLittleO.right_isBigO_sub ?_
simpa [div_eq_inv_mul, Function.comp_def] using
.atTop_of_const_mul₀ zero_lt_three (by simp [tendsto_natCast_atTop_atTop])
· rw [IsBigO_def]
refine ⟨12, ?_⟩
simp only [IsBigOWith, norm_natCast, eventually_atTop]
exact ⟨15, fun x hx ↦ by norm_cast; cutsat⟩
· rw [isBigO_exp_comp_exp_comp]
refine ⟨0, ?_⟩
simp only [neg_mul, eventually_map, Pi.sub_apply, sub_neg_eq_add, neg_add_le_iff_le_add, add_zero, ofNat_pos,
mul_le_mul_iff_right₀, eventually_atTop]
refine ⟨9, fun x hx ↦ ?_⟩
gcongr
· simp
cutsat
· cutsat
· refine .of_norm_eventuallyLE ?_
filter_upwards [eventually_ge_atTop 6] with n hn
have : (0 : ℝ) ≤ n / 3 - 2 := by rify at hn; linarith
simpa [neg_mul, abs_mul, abs_of_nonneg this] using ruzsaSzemerediNumberNat_lower_bound n
