English
In the closed interval Icc(a,b), the derivative of taylorWithinEval with respect to y exists within the interval, and is given by a scalar multiple of the next iterated derivative evaluated at t.
Русский
В замкнутом интервале Icc(a,b) производная taylorWithinEval по y существует внутри интервала и задаётся скалярным множителем следующей итеративной производной в точке t.
LaTeX
$$HasDerivWithinAt (fun y => taylorWithinEval f n (Icc a b) y x) ( ((n !)^{-1} * (x - t)^n) • iteratedDerivWithin (n+1) f (Icc a b) t) (Icc a b) t$$
Lean4
/-- Calculate the derivative of the Taylor polynomial with respect to `x₀`.
Version for closed intervals -/
theorem hasDerivWithinAt_taylorWithinEval_at_Icc {f : ℝ → E} {a b t : ℝ} (x : ℝ) {n : ℕ} (hx : a < b) (ht : t ∈ Icc a b)
(hf : ContDiffOn ℝ n f (Icc a b)) (hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Icc a b)) (Icc a b)) :
HasDerivWithinAt (fun y => taylorWithinEval f n (Icc a b) y x)
(((n ! : ℝ)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Icc a b) t) (Icc a b) t :=
hasDerivWithinAt_taylorWithinEval (uniqueDiffOn_Icc hx) self_mem_nhdsWithin ht rfl.subset hf (hf' t ht)
