English
A specialized form of exp_approx_succ for unit arguments (e.g., involving 1 and tail adjustments).
Русский
Узкоспециальная форма exp_approx_succ для единичных аргументов.
LaTeX
$$$|\\exp(1) - \\expNear(n, 1, a)| ≤ |1|^{n}/n! · b$ under suitable en and er constraints.$$
Lean4
theorem exp_bound_div_one_sub_of_interval' {x : ℝ} (h1 : 0 < x) (h2 : x < 1) : Real.exp x < 1 / (1 - x) :=
by
have H : 0 < 1 - (1 + x + x ^ 2) * (1 - x) :=
calc
0 < x ^ 3 := by positivity
_ = 1 - (1 + x + x ^ 2) * (1 - x) := by ring
calc
exp x ≤ _ := exp_bound' h1.le h2.le zero_lt_three
_ ≤ 1 + x + x ^ 2 := by
-- Porting note: was `norm_num [Finset.sum] <;> nlinarith`
-- This proof should be restored after the norm_num plugin for big operators is ported.
-- (It may also need the positivity extensions in https://github.com/leanprover-community/mathlib4/pull/3907.)
rw [show 3 = 1 + 1 + 1 from rfl]
repeat rw [Finset.sum_range_succ]
norm_num [Nat.factorial]
nlinarith
_ < 1 / (1 - x) := by rw [lt_div_iff₀] <;> nlinarith
