mathlib3documentation

analysis.calculus.taylor

Taylor's theorem #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

• taylor_coeff_within: the Taylor coefficient using deriv_within
• taylor_within: the Taylor polynomial using deriv_within

Main statements #

• taylor_mean_remainder: Taylor's theorem with the general form of the remainder term
• taylor_mean_remainder_lagrange: Taylor's theorem with the Lagrange remainder
• taylor_mean_remainder_cauchy: Taylor's theorem with the Cauchy remainder
• exists_taylor_mean_remainder_bound: Taylor's theorem for vector valued functions with a polynomial bound on the remainder

TODO #

• the Peano form of the remainder
• the integral form of the remainder
• Generalization to higher dimensions

Tags #

Taylor polynomial, Taylor's theorem

noncomputable def taylor_coeff_within {E : Type u_2} [ E] (f : E) (k : ) (s : set ) (x₀ : ) :
E

The kth coefficient of the Taylor polynomial.

Equations
noncomputable def taylor_within {E : Type u_2} [ 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
noncomputable def taylor_within_eval {E : Type u_2} [ 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
• s x₀ x = n s x₀)
theorem taylor_within_succ {E : Type u_2} [ E] (f : E) (n : ) (s : set ) (x₀ : ) :
(n + 1) s x₀ = s x₀ + ( (n + 1)) (n + 1) s x₀))
@[simp]
theorem taylor_within_eval_succ {E : Type u_2} [ E] (f : E) (n : ) (s : set ) (x₀ x : ) :
(n + 1) s x₀ x = s x₀ x + (((n + 1) * (n.factorial))⁻¹ * (x - x₀) ^ (n + 1)) iterated_deriv_within (n + 1) f s x₀
@[simp]
theorem taylor_within_zero_eval {E : Type u_2} [ E] (f : E) (s : set ) (x₀ x : ) :
s x₀ x = f x₀

The Taylor polynomial of order zero evaluates to f x.

@[simp]
theorem taylor_within_eval_self {E : Type u_2} [ E] (f : E) (n : ) (s : set ) (x₀ : ) :
s x₀ x₀ = f x₀

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

theorem taylor_within_apply {E : Type u_2} [ E] (f : E) (n : ) (s : set ) (x₀ x : ) :
s x₀ x = (finset.range (n + 1)).sum (λ (k : ), (((k.factorial))⁻¹ * (x - x₀) ^ k) x₀)
theorem continuous_on_taylor_within_eval {E : Type u_2} [ E] {f : E} {x : } {n : } {s : set } (hs : s) (hf : f s) :
continuous_on (λ (t : ), s t x) s

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

theorem monomial_has_deriv_aux (t x : ) (n : ) :
has_deriv_at (λ (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 has_deriv_within_at_taylor_coeff_within {E : Type u_2} [ E] {f : E} {x y : } {k : } {s t : set } (ht : y) (hs : s t) (hf : (iterated_deriv_within (k + 1) f s) s y) :
has_deriv_within_at (λ (z : ), (((k + 1) * (k.factorial))⁻¹ * (x - z) ^ (k + 1)) iterated_deriv_within (k + 1) f s z) ((((k + 1) * (k.factorial))⁻¹ * (x - y) ^ (k + 1)) iterated_deriv_within (k + 2) f s y - (((k.factorial))⁻¹ * (x - y) ^ k) iterated_deriv_within (k + 1) f s y) t y
theorem has_deriv_within_at_taylor_within_eval {E : Type u_2} [ E] {f : E} {x y : } {n : } {s s' : set } (hs'_unique : y) (hs_unique : s) (hs' : s' s) (hy : y s') (h : s' s) (hf : f s) (hf' : y) :
has_deriv_within_at (λ (t : ), s t x) ((((n.factorial))⁻¹ * (x - y) ^ n) iterated_deriv_within (n + 1) f s y) s' y

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

Version for arbitrary sets

theorem taylor_within_eval_has_deriv_at_Ioo {E : Type u_2} [ E] {f : E} {a b t : } (x : ) {n : } (hx : a < b) (ht : t b) (hf : f (set.Icc a b)) (hf' : (set.Icc a b)) (set.Ioo a b)) :
has_deriv_at (λ (y : ), (set.Icc a b) y x) ((((n.factorial))⁻¹ * (x - t) ^ n) iterated_deriv_within (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 has_deriv_within_taylor_within_eval_at_Icc {E : Type u_2} [ E] {f : E} {a b t : } (x : ) {n : } (hx : a < b) (ht : t b) (hf : f (set.Icc a b)) (hf' : (set.Icc a b)) (set.Icc a b)) :
has_deriv_within_at (λ (y : ), (set.Icc a b) y x) ((((n.factorial))⁻¹ * (x - t) ^ n) iterated_deriv_within (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 : f (set.Icc x₀ x)) (hf' : (set.Icc x₀ x)) (set.Ioo x₀ x)) (gcont : (set.Icc x₀ x)) (gdiff : (x_1 : ), x_1 set.Ioo x₀ x (g' x_1) x_1) (g'_ne : (x_1 : ), x_1 set.Ioo x₀ x g' x_1 0) :
(x' : ) (hx' : x' set.Ioo x₀ x), f x - (set.Icc x₀ x) x₀ x = ((x - x') ^ n / (n.factorial) * (g x - g x₀) / g' x') iterated_deriv_within (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 a 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 : f (set.Icc x₀ x)) (hf' : (set.Icc x₀ x)) (set.Ioo x₀ x)) :
(x' : ) (hx' : x' set.Ioo x₀ x), f x - (set.Icc x₀ x) x₀ x = iterated_deriv_within (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 a 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 : f (set.Icc x₀ x)) (hf' : (set.Icc x₀ x)) (set.Ioo x₀ x)) :
(x' : ) (hx' : x' set.Ioo x₀ x), f x - (set.Icc x₀ x) x₀ x = iterated_deriv_within (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 a 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} [ E] {f : E} {a b C x : } {n : } (hab : a b) (hf : (n + 1) f (set.Icc a b)) (hx : x b) (hC : (y : ), y b iterated_deriv_within (n + 1) f (set.Icc a b) y C) :
f x - (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} [ E] {f : E} {a b : } {n : } (hab : a b) (hf : (n + 1) f (set.Icc a b)) :
(C : ), (x : ), x b f x - (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).