English
The function f(n) = n / (log n)^2 is little-o of the identity function, i.e. f(n) = o(n) as n → ∞.
Русский
Функция f(n) = n / (log n)^2 есть малый порядок по отношению к n, то есть f(n) = o(n) при n → ∞.
LaTeX
$$$\dfrac{n}{(\log n)^2} = o(n) \quad (n \to \infty)$$$
Lean4
theorem isLittleO_self_div_log_id : (fun (n : ℕ) => n / log n ^ 2) =o[atTop] (fun (n : ℕ) => (n : ℝ)) := by
calc
(fun (n : ℕ) => (n : ℝ) / log n ^ 2)
_ = fun (n : ℕ) => (n : ℝ) * ((log n) ^ 2)⁻¹ := by simp_rw [div_eq_mul_inv]
_ =o[atTop] fun (n : ℕ) => (n : ℝ) * 1⁻¹ :=
by
refine IsBigO.mul_isLittleO (isBigO_refl _ _) ?_
refine IsLittleO.inv_rev ?_ (by simp)
calc
_ = (fun (_ : ℕ) => ((1 : ℝ) ^ 2)) := by simp
_ =o[atTop] (fun (n : ℕ) => (log n) ^ 2) :=
IsLittleO.pow (IsLittleO.natCast_atTop <| isLittleO_const_log_atTop) (by norm_num)
_ = (fun (n : ℕ) => (n : ℝ)) := by ext; simp
