English
Taking the derivative of taylorWithinEval at n+1 with respect to x yields the TaylorWithinEval of the derivative within f at order n, evaluated at x.
Русский
Для производной taylorWithinEval на n+1 по x мы получаем taylorWithinEval для производной внутри f порядка n, в точке x.
LaTeX
$$HasDerivAt (taylorWithinEval f (n+1) s x0) ( taylorWithinEval (derivWithin f s) n s x0 x )$$
Lean4
/-- Calculate the derivative of the Taylor polynomial with respect to `x`. -/
theorem hasDerivAt_taylorWithinEval_succ {x₀ x : ℝ} {s : Set ℝ} (f : ℝ → E) (n : ℕ) :
HasDerivAt (taylorWithinEval f (n + 1) s x₀) (taylorWithinEval (derivWithin f s) n s x₀ x) x :=
by
change HasDerivAt (fun x ↦ taylorWithinEval f _ s x₀ x) _ _
simp_rw [taylor_within_apply]
have :
∀ (i : ℕ) {c : ℝ} {c' : E},
HasDerivAt (fun x ↦ (c * (x - x₀) ^ i) • c') ((c * (i * (x - x₀) ^ (i - 1) * 1)) • c') x :=
fun _ _ ↦ hasDerivAt_id _ |>.sub_const _ |>.pow _ |>.const_mul _ |>.smul_const _
apply HasDerivAt.fun_sum (fun i _ => this i) |>.congr_deriv
rw [Finset.sum_range_succ', Nat.cast_zero, zero_mul, zero_mul, mul_zero, zero_smul, add_zero]
apply Finset.sum_congr rfl
intro i _
rw [← iteratedDerivWithin_succ']
congr 1
simp [field, Nat.factorial_succ]
