English
Let x ≥ 0. For every natural number n, the partial sum of the exponential series up to degree n−1 satisfies ∑_{i=0}^{n−1} x^i / i! ≤ exp(x).
Русский
Пусть x ≥ 0. Для каждого натурального n частичная сумма экспоненциального ряда до степени n−1 удовлетворяет неравенству ∑_{i=0}^{n−1} x^i / i! ≤ exp(x).
LaTeX
$$$\sum_{i=0}^{n-1} \frac{x^i}{i!} \le \exp x$$$
Lean4
theorem sum_le_exp_of_nonneg {x : ℝ} (hx : 0 ≤ x) (n : ℕ) : ∑ i ∈ range n, x ^ i / i ! ≤ exp x :=
calc
∑ i ∈ range n, x ^ i / i ! ≤ lim (⟨_, isCauSeq_re (exp' x)⟩ : CauSeq ℝ abs) :=
by
refine le_lim (CauSeq.le_of_exists ⟨n, fun j hj => ?_⟩)
simp only [exp', const_apply, re_sum]
norm_cast
refine sum_le_sum_of_subset_of_nonneg (range_mono hj) fun _ _ _ ↦ ?_
positivity
_ = exp x := by rw [exp, Complex.exp, ← cauSeqRe, lim_re]
