Theorems · Theorem · global analysis

hasDerivWithinAt_taylor_coeff_within

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

Defined in

Mathlib.Analysis.Calculus.Taylor

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace