English
For each i, the smoothing difference ε(b_i n) − ε(n) is Theta of 1/(log n)^2 as n → ∞.
Русский
Для каждого i разность ε(b_i n) − ε(n) имеет порядок Θ(1/(log n)^2) при n → ∞.
LaTeX
$$$$ε(b_i n) - ε(n) = Θ\left(\frac{1}{(\log n)^2}\right)\quad(n\to\infty).$$$$
Lean4
theorem isTheta_smoothingFn_sub_self (i : α) : (fun (n : ℕ) => ε (b i * n) - ε n) =Θ[atTop] fun n => 1 / (log n) ^ 2 :=
by
calc
(fun (n : ℕ) => ε (b i * n) - ε n)
_ =Θ[atTop] fun n => (-log (b i)) / (log n) ^ 2 := (R.isEquivalent_smoothingFn_sub_self i).isTheta
_ = fun (n : ℕ) => (-log (b i)) * 1 / (log n) ^ 2 := by simp only [mul_one]
_ = fun (n : ℕ) => -log (b i) * (1 / (log n) ^ 2) := by simp_rw [← mul_div_assoc]
_ =Θ[atTop] fun (n : ℕ) => 1 / (log n) ^ 2 :=
by
have : -log (b i) ≠ 0 := by
rw [neg_ne_zero]
exact Real.log_ne_zero_of_pos_of_ne_one (R.b_pos i) (ne_of_lt <| R.b_lt_one i)
rw [← isTheta_const_mul_right this]
