English
If 0 ≤ x ≤ 1 and n > 0, then exp x ≤ ∑_{m=0}^{n-1} x^m/m! + x^n · (n+1)/(n! · n).
Русский
Если 0 ≤ x ≤ 1 и n > 0, то exp x ≤ сумма первых n членов плюс дополнительный член.
LaTeX
$$$\\exp x \\leq \\sum_{m=0}^{n-1} \\frac{x^{m}}{m!} + x^{n} \\cdot \\frac{n+1}{n! \\; n}.$$$
Lean4
theorem exp_bound' {x : ℝ} (h1 : 0 ≤ x) (h2 : x ≤ 1) {n : ℕ} (hn : 0 < n) :
Real.exp x ≤ (∑ m ∈ Finset.range n, x ^ m / m.factorial) + x ^ n * (n + 1) / (n.factorial * n) :=
by
have h3 : |x| = x := by simpa
have h4 : |x| ≤ 1 := by rwa [h3]
have h' := Real.exp_bound h4 hn
rw [h3] at h'
have h'' := (abs_sub_le_iff.1 h').1
have t := sub_le_iff_le_add'.1 h''
simpa [mul_div_assoc] using t
