Theorems · Theorem · global analysis

taylorWithinEval_succ

∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (f : ℝ → E) (n : ℕ) (s : Set ℝ) (x₀ x : ℝ),
  taylorWithinEval f (n + 1) s x₀ x =
    taylorWithinEval f n s x₀ x +
      (((↑n + 1) * ↑n.factorial)⁻¹ * (x - x₀) ^ (n + 1)) • iteratedDerivWithin (n + 1) f s x₀

Defined in

Mathlib.Analysis.Calculus.Taylor

Cited by

6 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace