English
Applying the Taylor operator up to order n+1 yields the sum of terms up to order n plus the next-order residual term expressed via the coefficient taylorCoeffWithin.
Русский
Применение оператора Тейлора до порядка n+1 даёт сумму членов до n-го порядка плюс остаток следующего порядка через коэффициент taylorCoeffWithin.
LaTeX
$$$taylorWithin(f,n+1,s,x_0) = taylorWithin(f,n,s,x_0) + (X - C x_0) \cdot taylorCoeffWithin(f,n+1,s,x_0)$$$
Lean4
theorem taylor_within_apply (f : ℝ → E) (n : ℕ) (s : Set ℝ) (x₀ x : ℝ) :
taylorWithinEval f n s x₀ x =
∑ k ∈ Finset.range (n + 1), ((k ! : ℝ)⁻¹ * (x - x₀) ^ k) • iteratedDerivWithin k f s x₀ :=
by
induction n with
| zero => simp
| succ k hk =>
rw [taylorWithinEval_succ, Finset.sum_range_succ, hk]
simp [Nat.factorial]
