Theorems · Theorem · global analysis

hasDerivWithinAt_taylorWithinEval

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

Calculate the derivative of the Taylor polynomial with respect to x₀. Version for arbitrary sets

Defined in

Mathlib.Analysis.Calculus.Taylor

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace