English
Define a smoothing function ε(n) = 1 / log n. This function tends to 0 as n → ∞.
Русский
Определим сглаживающую функцию ε(n) = 1 / log n. Эта функция стремится к 0 при n → ∞.
LaTeX
$$$\varepsilon(n) = \dfrac{1}{\log n}$ and \; \varepsilon(n) \to 0 \; (n\to\infty)$$$
Lean4
theorem eventually_bi_mul_le_r : ∀ᶠ (n : ℕ) in atTop, ∀ i, (b (min_bi b) / 2) * n ≤ r i n :=
by
have gt_zero : 0 < b (min_bi b) := R.b_pos (min_bi b)
have hlo := isLittleO_self_div_log_id
rw [Asymptotics.isLittleO_iff] at hlo
have hlo' := hlo (by positivity : 0 < b (min_bi b) / 2)
filter_upwards [hlo', R.eventually_b_le_r] with n hn hn' i
simp only [Real.norm_of_nonneg (by positivity : 0 ≤ (n : ℝ))] at hn
calc
b (min_bi b) / 2 * n
_ = b (min_bi b) * n - b (min_bi b) / 2 * n := by ring
_ ≤ b (min_bi b) * n - ‖n / log n ^ 2‖ := by gcongr
_ ≤ b i * n - ‖n / log n ^ 2‖ := by gcongr; aesop
_ = b i * n - n / log n ^ 2 := by
congr
exact Real.norm_of_nonneg <| by positivity
_ ≤ r i n := hn' i
