Theorems · Theorem · global analysis

taylor_mean_remainder_bound

∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b C x : ℝ} {n : ℕ},
  a ≤ b →
    ContDiffOn ℝ (↑n + 1) f (Set.Icc a b) →
      x ∈ Set.Icc a b →
        (∀ y ∈ Set.Icc a b, ‖iteratedDerivWithin (n + 1) f (Set.Icc a b) y‖ ≤ C) →
          ‖f x - taylorWithinEval f n (Set.Icc a b) a x‖ ≤ C * (x - a) ^ (n + 1) / ↑n.factorial

Taylor's theorem with a polynomial bound on the remainder We assume that f is n+1-times continuously differentiable on the closed set Icc a b. The difference of f and its n-th Taylor polynomial can be estimated by C * (x - a)^(n+1) / n! where C is a bound for the n+1-th iterated derivative of f.

Defined in

Mathlib.Analysis.Calculus.Taylor

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace