English
For each i, the difference ε(b_i n) − ε(n) is asymptotically equivalent to −log(b_i)/(log n)^2 as n → ∞.
Русский
Для каждого i различие ε(b_i n) − ε(n) асимптотически эквивалентно −log(b_i)/(log n)^2 при n → ∞.
LaTeX
$$$$\forall i,\; ε(b_i n) - ε(n) \sim -\frac{\log(b_i)}{(\log n)^2} \quad (n\to\infty).$$$$
Lean4
theorem isLittleO_deriv_smoothingFn : deriv ε =o[atTop] fun x => x⁻¹ :=
calc
deriv ε
_ =ᶠ[atTop] fun x => -x⁻¹ / (log x ^ 2) :=
by
filter_upwards [eventually_gt_atTop 1] with x hx
rw [deriv_smoothingFn hx]
_ = fun x => (-x * log x ^ 2)⁻¹ := by simp_rw [neg_div, div_eq_mul_inv, ← mul_inv, neg_inv, neg_mul]
_ =o[atTop] fun x => (x * 1)⁻¹ := by
refine IsLittleO.inv_rev ?_ ?_
· refine IsBigO.mul_isLittleO (by rw [isBigO_neg_right]; aesop (add safe isBigO_refl)) ?_
rw [isLittleO_one_left_iff]
exact Tendsto.comp tendsto_norm_atTop_atTop <| Tendsto.comp (tendsto_pow_atTop (by norm_num)) tendsto_log_atTop
· exact Filter.Eventually.of_forall (fun x hx => by rw [mul_one] at hx; simp [hx])
_ = fun x => x⁻¹ := by simp
