exp_neg_two_mul_le — Mathlib

English

Let x be a positive real number. Then e^(−2x) < e^(2 − ⌈x⌉) / ⌈x⌉.

Русский

Пусть x > 0. Тогда e^(−2x) < e^(2 − ⌈x⌉) / ⌈x⌉.

LaTeX

$$$$ \\exp(-2x) < \\frac{\\exp\\left(2 - \\lceil x \\rceil \\right)}{\\lceil x \\rceil} \\qquad (x > 0) $$$$

Lean4

theorem exp_neg_two_mul_le {x : ℝ} (hx : 0 < x) : exp (-2 * x) < exp (2 - ⌈x⌉₊) / ⌈x⌉₊ :=
  by
  have h₁ := ceil_lt_add_one hx.le
  have h₂ : 1 - x ≤ 2 - ⌈x⌉₊ := by linarith
  calc
    _ ≤ exp (1 - x) / (x + 1) := ?_
    _ ≤ exp (2 - ⌈x⌉₊) / (x + 1) := by gcongr
    _ < _ := by gcongr
  rw [le_div_iff₀ (add_pos hx zero_lt_one), ← le_div_iff₀' (exp_pos _), ← exp_sub, neg_mul, sub_neg_eq_add, two_mul,
    sub_add_add_cancel, add_comm _ x]
  exact le_trans (le_add_of_nonneg_right zero_le_one) (add_one_le_exp _)

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