one_add_smoothingFn_le_two — Mathlib

English

For x large enough, 1 + smoothingFn(x) ≤ 2.

Русский

Для достаточно больших x верно 1 + сглаживающая функция(x) ≤ 2.

LaTeX

$$$1 + \varepsilon(x) \le 2 \quad (x \ge e)$$$

Lean4

theorem one_add_smoothingFn_le_two {x : ℝ} (hx : exp 1 ≤ x) : 1 + ε x ≤ 2 :=
  by
  simp only [smoothingFn, ← one_add_one_eq_two]
  gcongr
  have : 1 < x := by
    calc
      1 = exp 0 := by simp
      _ < exp 1 := by simp
      _ ≤ x := hx
  rw [div_le_one (log_pos this)]
  calc
    1 = log (exp 1) := by simp
    _ ≤ log x := log_le_log (exp_pos _) hx

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