exp_1_approx_succ_eq — Mathlib

English

A generalized form of exp_approx_end with a third parameter and a relation between remainders, yielding a bound.

Русский

Обобщенная форма exp_approx_end с третьим параметром и зависимостью между остатками даёт ограничение.

LaTeX

$$$|\\exp x - \\expNear n x a| \\leq |x|^{n}/n! · b$ under appropriate relation between a,b and tail parameters.$$

Lean4

theorem exp_1_approx_succ_eq {n} {a₁ b₁ : ℝ} {m : ℕ} (en : n + 1 = m) {rm : ℝ} (er : ↑m = rm)
    (h : |exp 1 - expNear m 1 ((a₁ - 1) * rm)| ≤ |1| ^ m / m.factorial * (b₁ * rm)) :
    |exp 1 - expNear n 1 a₁| ≤ |1| ^ n / n.factorial * b₁ :=
  by
  subst er
  refine exp_approx_succ _ en _ _ ?_ h
  field_simp [show (m : ℝ) ≠ 0 by norm_cast; cutsat]
  simp

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