English
The k-th term in the Taylor evaluation is given by the k-th iterated derivative within the set, divided by k!, multiplied by (x−x0)^k.
Русский
СтрокаTaylor состоит из k-й итераированной производной внутри множества, делённой на k!, умноженной на (x−x0)^k.
LaTeX
$$$taylorWithinEval\ f\ n\ s\ x_0\ x=\sum_{k=0}^{n}\Big(\frac{(x-x_0)^k}{k!}\Big)\cdot \ iteratedDerivWithin(k)f\ s\ x_0$$$
Lean4
@[simp]
theorem taylorWithinEval_succ (f : ℝ → E) (n : ℕ) (s : Set ℝ) (x₀ x : ℝ) :
taylorWithinEval f (n + 1) s x₀ x =
taylorWithinEval f n s x₀ x + (((n + 1 : ℝ) * n !)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀ :=
by
simp_rw [taylorWithinEval, taylorWithin_succ, LinearMap.map_add, PolynomialModule.comp_eval]
congr
simp only [Polynomial.eval_sub, Polynomial.eval_X, Polynomial.eval_C, PolynomialModule.eval_single, mul_inv_rev]
dsimp only [taylorCoeffWithin]
rw [← mul_smul, mul_comm, Nat.factorial_succ, Nat.cast_mul, Nat.cast_add, Nat.cast_one, mul_inv_rev]
