English
The Taylor polynomial of degree n+1 is obtained from the degree n polynomial by adding a correction term corresponding to the (n+1)-th coefficient.
Русский
Тейлоров полином степени n+1 равен полиному степень n плюс поправка, соответствующая коэффициенту при степени n+1.
LaTeX
$$$taylorWithin f (n+1) s x_0 = taylorWithin f n s x_0 + \\\\ PolynomialModule.comp (Polynomial.X - Polynomial.C x_0) \\\\ (PolynomialModule.single \\mathbb{R} (n+1) (taylorCoeffWithin f (n+1) s x_0))$$$
Lean4
theorem taylorWithin_succ (f : ℝ → E) (n : ℕ) (s : Set ℝ) (x₀ : ℝ) :
taylorWithin f (n + 1) s x₀ =
taylorWithin f n s x₀ +
PolynomialModule.comp (Polynomial.X - Polynomial.C x₀)
(PolynomialModule.single ℝ (n + 1) (taylorCoeffWithin f (n + 1) s x₀)) :=
by
dsimp only [taylorWithin]
rw [Finset.sum_range_succ]
