abs_log_mul_self_rpow_lt — Mathlib

English

For 0 < x ≤ 1 and t > 0, |log x · x^t| < 1/t.

Русский

Пусть 0 < x ≤ 1 и t > 0, тогда |log x · x^t| < 1/t.

LaTeX

$$For x ∈ (0,1], t > 0, |log x · x^t| < 1 / t$$

Lean4

/-- Bound for `|log x * x ^ t|` in the interval `(0, 1]`, for positive real `t`. -/
theorem abs_log_mul_self_rpow_lt (x t : ℝ) (h1 : 0 < x) (h2 : x ≤ 1) (ht : 0 < t) : |log x * x ^ t| < 1 / t :=
  by
  rw [lt_div_iff₀ ht]
  have := abs_log_mul_self_lt (x ^ t) (rpow_pos_of_pos h1 t) (rpow_le_one h1.le h2 ht.le)
  rwa [log_rpow h1, mul_assoc, abs_mul, abs_of_pos ht, mul_comm] at this

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