English
For open interval Ioo(a,b), the derivative of taylorWithinEval at t equals the appropriate multiple of the next iterated derivative inside the interval evaluated at t.
Русский
Для открытого интервала Ioo(a,b) производная taylorWithinEval в точке t равна нужному множителю следующей итеративной производной внутри интервала, взятой в t.
LaTeX
$$HasDerivAt (fun y => taylorWithinEval f n (Ioo a b) y x) ( ((n!)^{-1}*(x - t)^n) • iteratedDerivWithin(n+1) f (Icc a b) t) t$$
Lean4
/-- Calculate the derivative of the Taylor polynomial with respect to `x₀`.
Version for open intervals -/
theorem taylorWithinEval_hasDerivAt_Ioo {f : ℝ → E} {a b t : ℝ} (x : ℝ) {n : ℕ} (hx : a < b) (ht : t ∈ Ioo a b)
(hf : ContDiffOn ℝ n f (Icc a b)) (hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Ioo a b)) :
HasDerivAt (fun y => taylorWithinEval f n (Icc a b) y x)
(((n ! : ℝ)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) t) t :=
have h_nhds : Ioo a b ∈ 𝓝 t := isOpen_Ioo.mem_nhds ht
have h_nhds' : Ioo a b ∈ 𝓝[Icc a b] t := nhdsWithin_le_nhds h_nhds
(hasDerivWithinAt_taylorWithinEval (uniqueDiffOn_Icc hx) h_nhds' ht Ioo_subset_Icc_self hf <|
(hf' t ht).mono_of_mem_nhdsWithin h_nhds').hasDerivAt
h_nhds
