rpow_inv_log_le_exp_one — Mathlib

English

For all x > 0, x^{(log x)^{-1}} ≤ e.

Русский

Для всех x > 0 выполняется x^{(log x)^{-1}} ≤ e.

LaTeX

$$$\\forall x \\in \\mathbb{R}, x > 0 \\Rightarrow x^{(\\log x)^{-1}} \\le e$$$

Lean4

/-- See `Real.rpow_inv_log` for the equality when `x ≠ 1` is strictly positive. -/
theorem rpow_inv_log_le_exp_one : x ^ (log x)⁻¹ ≤ exp 1 :=
  by
  calc
    _ ≤ |x ^ (log x)⁻¹| := le_abs_self _
    _ ≤ |x| ^ (log x)⁻¹ := abs_rpow_le_abs_rpow ..
  rw [← log_abs]
  obtain hx | hx := (abs_nonneg x).eq_or_lt'
  · simp [hx]
  · rw [rpow_def_of_pos hx]
    gcongr
    exact mul_inv_le_one

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