quadratic_le_exp_of_nonneg — Mathlib

English

Let x ≥ 0. Then 1 + x + x^2/2 ≤ exp(x).

Русский

Пусть x ≥ 0. Тогда 1 + x + x^2/2 ≤ exp(x).

LaTeX

$$$1 + x + \frac{x^2}{2} \le \exp x$$$

Lean4

theorem quadratic_le_exp_of_nonneg {x : ℝ} (hx : 0 ≤ x) : 1 + x + x ^ 2 / 2 ≤ exp x :=
  calc
    1 + x + x ^ 2 / 2 = ∑ i ∈ range 3, x ^ i / i ! :=
      by
      simp only [sum_range_succ, range_one, sum_singleton, _root_.pow_zero, factorial, pow_one, mul_one, Nat.mul_one,
        cast_succ]
      ring_nf
    _ ≤ exp x := sum_le_exp_of_nonneg hx 3

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