norm_log_natCast_le_rpow_div — Mathlib

English

For natural number n and ε > 0, |log n| ≤ n^ε / ε.

Русский

Для натурального n и ε > 0 выполнено |log n| ≤ n^ε / ε.

LaTeX

$$Let n ∈ ℕ and ε > 0. |log n| ≤ n^ε / ε.$$

Lean4

theorem norm_log_natCast_le_rpow_div (n : ℕ) {ε : ℝ} (hε : 0 < ε) : ‖log n‖ ≤ n ^ ε / ε :=
  by
  rcases n.eq_zero_or_pos with rfl | h
  · rw [Nat.cast_zero, Nat.cast_zero, log_zero, norm_zero, Real.zero_rpow hε.ne', zero_div]
  rw [← natCast_log, norm_real, norm_of_nonneg <| Real.log_nonneg <| by exact_mod_cast Nat.one_le_of_lt h.lt]
  exact Real.log_natCast_le_rpow_div n hε

Похожие утверждения