Documentation

Mathlib.Analysis.Calculus.Taylor

Taylor's theorem #

This file defines the Taylor polynomial of a real function f : ℝ → E, where E is a normed vector space over and proves Taylor's theorem, which states that if f is sufficiently smooth, then f can be approximated by the Taylor polynomial up to an explicit error term.

Main definitions #

Main statements #

TODO #

Tags #

Taylor polynomial, Taylor's theorem

noncomputable def taylorCoeffWithin {E : Type u_2} [NormedAddCommGroup E] [NormedSpace E] (f : E) (k : ) (s : Set ) (x₀ : ) :
E

The kth coefficient of the Taylor polynomial.

Equations
Instances For
    noncomputable def taylorWithin {E : Type u_2} [NormedAddCommGroup E] [NormedSpace E] (f : E) (n : ) (s : Set ) (x₀ : ) :

    The Taylor polynomial with derivatives inside of a set s.

    The Taylor polynomial is given by $$∑_{k=0}^n \frac{(x - x₀)^k}{k!} f^{(k)}(x₀),$$ where $f^{(k)}(x₀)$ denotes the iterated derivative in the set s.

    Equations
    Instances For
      noncomputable def taylorWithinEval {E : Type u_2} [NormedAddCommGroup E] [NormedSpace E] (f : E) (n : ) (s : Set ) (x₀ : ) (x : ) :
      E

      The Taylor polynomial with derivatives inside of a set s considered as a function ℝ → E

      Equations
      Instances For
        theorem taylorWithin_succ {E : Type u_2} [NormedAddCommGroup E] [NormedSpace E] (f : E) (n : ) (s : Set ) (x₀ : ) :
        taylorWithin f (n + 1) s x₀ = taylorWithin f n s x₀ + (PolynomialModule.comp (Polynomial.X - Polynomial.C x₀)) ((PolynomialModule.single (n + 1)) (taylorCoeffWithin f (n + 1) s x₀))
        @[simp]
        theorem taylorWithinEval_succ {E : Type u_2} [NormedAddCommGroup E] [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₀
        @[simp]
        theorem taylor_within_zero_eval {E : Type u_2} [NormedAddCommGroup E] [NormedSpace E] (f : E) (s : Set ) (x₀ : ) (x : ) :
        taylorWithinEval f 0 s x₀ x = f x₀

        The Taylor polynomial of order zero evaluates to f x.

        @[simp]
        theorem taylorWithinEval_self {E : Type u_2} [NormedAddCommGroup E] [NormedSpace E] (f : E) (n : ) (s : Set ) (x₀ : ) :
        taylorWithinEval f n s x₀ x₀ = f x₀

        Evaluating the Taylor polynomial at x = x₀ yields f x.

        theorem taylor_within_apply {E : Type u_2} [NormedAddCommGroup E] [NormedSpace E] (f : E) (n : ) (s : Set ) (x₀ : ) (x : ) :
        taylorWithinEval f n s x₀ x = kFinset.range (n + 1), ((↑k.factorial)⁻¹ * (x - x₀) ^ k) iteratedDerivWithin k f s x₀
        theorem continuousOn_taylorWithinEval {E : Type u_2} [NormedAddCommGroup E] [NormedSpace E] {f : E} {x : } {n : } {s : Set } (hs : UniqueDiffOn s) (hf : ContDiffOn (↑n) f s) :
        ContinuousOn (fun (t : ) => taylorWithinEval f n s t x) s

        If f is n times continuous differentiable on a set s, then the Taylor polynomial taylorWithinEval f n s x₀ x is continuous in x₀.

        theorem monomial_has_deriv_aux (t : ) (x : ) (n : ) :
        HasDerivAt (fun (y : ) => (x - y) ^ (n + 1)) (-(n + 1) * (x - t) ^ n) t

        Helper lemma for calculating the derivative of the monomial that appears in Taylor expansions.

        theorem hasDerivWithinAt_taylor_coeff_within {E : Type u_2} [NormedAddCommGroup E] [NormedSpace E] {f : E} {x : } {y : } {k : } {s : Set } {t : Set } (ht : UniqueDiffWithinAt t y) (hs : s nhdsWithin y t) (hf : 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
        theorem hasDerivWithinAt_taylorWithinEval {E : Type u_2} [NormedAddCommGroup E] [NormedSpace E] {f : E} {x : } {y : } {n : } {s : Set } {s' : Set } (hs'_unique : UniqueDiffWithinAt s' y) (hs_unique : UniqueDiffOn s) (hs' : s' nhdsWithin y s) (hy : y s') (h : s' s) (hf : ContDiffOn (↑n) f s) (hf' : DifferentiableWithinAt (iteratedDerivWithin n f s) s y) :
        HasDerivWithinAt (fun (t : ) => taylorWithinEval f n s t x) (((↑n.factorial)⁻¹ * (x - y) ^ n) iteratedDerivWithin (n + 1) f s y) s' y

        Calculate the derivative of the Taylor polynomial with respect to x₀.

        Version for arbitrary sets

        theorem taylorWithinEval_hasDerivAt_Ioo {E : Type u_2} [NormedAddCommGroup E] [NormedSpace E] {f : E} {a : } {b : } {t : } (x : ) {n : } (hx : a < b) (ht : t Set.Ioo a b) (hf : ContDiffOn (↑n) f (Set.Icc a b)) (hf' : DifferentiableOn (iteratedDerivWithin n f (Set.Icc a b)) (Set.Ioo a b)) :
        HasDerivAt (fun (y : ) => taylorWithinEval f n (Set.Icc a b) y x) (((↑n.factorial)⁻¹ * (x - t) ^ n) iteratedDerivWithin (n + 1) f (Set.Icc a b) t) t

        Calculate the derivative of the Taylor polynomial with respect to x₀.

        Version for open intervals

        theorem hasDerivWithinAt_taylorWithinEval_at_Icc {E : Type u_2} [NormedAddCommGroup E] [NormedSpace E] {f : E} {a : } {b : } {t : } (x : ) {n : } (hx : a < b) (ht : t Set.Icc a b) (hf : ContDiffOn (↑n) f (Set.Icc a b)) (hf' : DifferentiableOn (iteratedDerivWithin n f (Set.Icc a b)) (Set.Icc a b)) :
        HasDerivWithinAt (fun (y : ) => taylorWithinEval f n (Set.Icc a b) y x) (((↑n.factorial)⁻¹ * (x - t) ^ n) iteratedDerivWithin (n + 1) f (Set.Icc a b) t) (Set.Icc a b) t

        Calculate the derivative of the Taylor polynomial with respect to x₀.

        Version for closed intervals

        Taylor's theorem with mean value type remainder estimate #

        theorem taylor_mean_remainder {f : } {g : } {g' : } {x : } {x₀ : } {n : } (hx : x₀ < x) (hf : ContDiffOn (↑n) f (Set.Icc x₀ x)) (hf' : DifferentiableOn (iteratedDerivWithin n f (Set.Icc x₀ x)) (Set.Ioo x₀ x)) (gcont : ContinuousOn g (Set.Icc x₀ x)) (gdiff : x_1Set.Ioo x₀ x, HasDerivAt g (g' x_1) x_1) (g'_ne : x_1Set.Ioo x₀ x, g' x_1 0) :
        x'Set.Ioo x₀ x, f x - taylorWithinEval f n (Set.Icc x₀ x) x₀ x = ((x - x') ^ n / n.factorial * (g x - g x₀) / g' x') iteratedDerivWithin (n + 1) f (Set.Icc x₀ x) x'

        Taylor's theorem with the general mean value form of the remainder.

        We assume that f is n+1-times continuously differentiable in the closed set Icc x₀ x and n+1-times differentiable on the open set Ioo x₀ x, and g is a differentiable function on Ioo x₀ x and continuous on Icc x₀ x. Then there exists an x' ∈ Ioo 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$.

        theorem taylor_mean_remainder_lagrange {f : } {x : } {x₀ : } {n : } (hx : x₀ < x) (hf : ContDiffOn (↑n) f (Set.Icc x₀ x)) (hf' : DifferentiableOn (iteratedDerivWithin n f (Set.Icc x₀ x)) (Set.Ioo x₀ x)) :
        x'Set.Ioo x₀ x, f x - taylorWithinEval f n (Set.Icc x₀ x) x₀ x = iteratedDerivWithin (n + 1) f (Set.Icc 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+1-times continuously differentiable in the closed set Icc x₀ x and n+1-times differentiable on the open set Ioo x₀ x. Then there exists an x' ∈ Ioo 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.

        theorem taylor_mean_remainder_cauchy {f : } {x : } {x₀ : } {n : } (hx : x₀ < x) (hf : ContDiffOn (↑n) f (Set.Icc x₀ x)) (hf' : DifferentiableOn (iteratedDerivWithin n f (Set.Icc x₀ x)) (Set.Ioo x₀ x)) :
        x'Set.Ioo x₀ x, f x - taylorWithinEval f n (Set.Icc x₀ x) x₀ x = iteratedDerivWithin (n + 1) f (Set.Icc x₀ x) x' * (x - x') ^ n / n.factorial * (x - x₀)

        Taylor's theorem with the Cauchy form of the remainder.

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

        theorem taylor_mean_remainder_bound {E : Type u_2} [NormedAddCommGroup E] [NormedSpace E] {f : E} {a : } {b : } {C : } {x : } {n : } (hab : a b) (hf : ContDiffOn (n + 1) f (Set.Icc a b)) (hx : x Set.Icc a b) (hC : ySet.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.

        theorem exists_taylor_mean_remainder_bound {E : Type u_2} [NormedAddCommGroup E] [NormedSpace E] {f : E} {a : } {b : } {n : } (hab : a b) (hf : ContDiffOn (n + 1) f (Set.Icc a b)) :
        ∃ (C : ), xSet.Icc a b, f x - taylorWithinEval f n (Set.Icc a b) a x C * (x - a) ^ (n + 1)

        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. There exists a constant C such that for all x ∈ Icc a b the difference of f and its n-th Taylor polynomial can be estimated by C * (x - a)^(n+1).