Theorems · Theorem · global analysis

hasDerivWithinAt_taylorWithinEval_at_Icc

∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b t : ℝ} (x : ℝ) {n : ℕ},
  a < b →
    t ∈ Set.Icc a b →
      ContDiffOn ℝ (↑n) f (Set.Icc a b) →
        DifferentiableOn ℝ (iteratedDerivWithin n f (Set.Icc a b)) (Set.Icc a b) →
          HasDerivWithinAt (fun y => taylorWithinEval f n (Set.Icc a b) y x)
            (((↑n.factorial)⁻¹ * (x - t) ^ n) • iteratedDerivWithin (n + 1) f (Set.Icc a b) t) (Set.Icc a b) t

Calculate the derivative of the Taylor polynomial with respect to x₀. Version for closed intervals

Defined in

Mathlib.Analysis.Calculus.Taylor

Cited by

1 results in Mathlib

Foundations

Depth 190 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpace