Theorems · Theorem · global analysis

taylor_mean_remainder

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

Taylor's theorem with the general mean value 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, and g is a differentiable function on uIoo x₀ x and continuous on uIcc x₀ x. Then there exists an x' ∈ uIoo x₀ x such that $$f(x) - (P_n f)(x₀, x) = \frac{(x - x')^n}{n!} \frac{g(x) - g(x₀)}{g' x'},$$ where $P_n f$ denotes the Taylor polynomial of degree $n$.

Defined in

Mathlib.Analysis.Calculus.Taylor

Cited by

2 results in Mathlib

Foundations

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