pow_div_factorial_le_exp — Mathlib

English

Let x ≥ 0. For every n ∈ ℕ, the term x^n / n! is bounded above by exp(x).

Русский

Пусть x ≥ 0. Для каждого n ∈ ℕ верно, что x^n / n! ≤ exp(x).

LaTeX

$$$\frac{x^n}{n!} \le \exp x$$$

Lean4

theorem pow_div_factorial_le_exp (hx : 0 ≤ x) (n : ℕ) : x ^ n / n ! ≤ exp x :=
  calc
    x ^ n / n ! ≤ ∑ k ∈ range (n + 1), x ^ k / k ! :=
      single_le_sum (f := fun k ↦ x ^ k / k !) (fun k _ ↦ by positivity) (self_mem_range_succ n)
    _ ≤ exp x := sum_le_exp_of_nonneg hx _

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