abs_log_mul_self_lt — Mathlib

English

For 0 < x ≤ 1, |log x · x| < 1.

Русский

Для 0 < x ≤ 1 верно |log x · x| < 1.

LaTeX

$$$0 < x \\\\le 1 \\\\Rightarrow |\\\\log x \\\\cdot x| < 1$$$

Lean4

/-- Bound for `|log x * x|` in the interval `(0, 1]`. -/
theorem abs_log_mul_self_lt (x : ℝ) (h1 : 0 < x) (h2 : x ≤ 1) : |log x * x| < 1 :=
  by
  have : 0 < 1 / x := by simpa only [one_div, inv_pos] using h1
  replace := log_le_sub_one_of_pos this
  replace : log (1 / x) < 1 / x := by linarith
  rw [log_div one_ne_zero h1.ne', log_one, zero_sub, lt_div_iff₀ h1] at this
  have aux : 0 ≤ -log x * x := by
    refine mul_nonneg ?_ h1.le
    rw [← log_inv]
    apply log_nonneg
    rw [← le_inv_comm₀ h1 zero_lt_one, inv_one]
    exact h2
  rw [← abs_of_nonneg aux, neg_mul, abs_neg] at this
  exact this

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