log_le_rpow_div — Mathlib

English

For x ≥ 0 and ε > 0, log x ≤ x^ε / ε.

Русский

Для x ≥ 0 и ε > 0 верно log x ≤ x^ε / ε.

LaTeX

$$For x ≥ 0, ε > 0, log x ≤ x^ε / ε$$

Lean4

/-- `log x` is bounded above by a multiple of every power of `x` with positive exponent. -/
theorem log_le_rpow_div {x ε : ℝ} (hx : 0 ≤ x) (hε : 0 < ε) : log x ≤ x ^ ε / ε :=
  by
  rcases hx.eq_or_lt with rfl | h
  · rw [log_zero, zero_rpow hε.ne', zero_div]
  rw [le_div_iff₀' hε]
  exact (log_rpow h ε).symm.trans_le <| (log_le_sub_one_of_pos <| rpow_pos_of_pos h ε).trans (sub_one_lt _).le

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