Theorems · Theorem · global analysis

taylor_mean_remainder_lagrange

• #35 of the 100 theorems: Taylor’s Theorem
• 1000+ list: Taylor's theorem

∀ {f : ℝ → ℝ} {x x₀ : ℝ} {n : ℕ},
  x₀ ≠ x →
    ContDiffOn ℝ (↑n) f (Set.uIcc x₀ x) →
      DifferentiableOn ℝ (iteratedDerivWithin n f (Set.uIcc x₀ x)) (Set.uIoo x₀ x) →
        ∃ x' ∈ Set.uIoo x₀ x,
          f x - taylorWithinEval f n (Set.uIcc x₀ x) x₀ x =
            iteratedDerivWithin (n + 1) f (Set.uIcc x₀ x) x' * (x - x₀) ^ (n + 1) / ↑(n + 1).factorial

Taylor's theorem with the Lagrange form of the remainder. We assume that f is n-times continuously differentiable in the closed set uIcc x₀ x and n+1-times differentiable on the open set uIoo x₀ x. Then there exists an x' ∈ uIoo x₀ x such that $$f(x) - (P_n f)(x₀, x) = \frac{f^{(n+1)}(x') (x - x₀)^{n+1}}{(n+1)!},$$ where $P_n f$ denotes the Taylor polynomial of degree $n$ and $f^{(n+1)}$ is the $n+1$-th iterated derivative.

Defined in

Mathlib.Analysis.Calculus.Taylor

Cited by

1 results in Mathlib

Foundations

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