mathlib3 documentation

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} [normed_add_comm_group E] [normed_space ℝ E] (f : ℝ → E) (k : ℕ) (s : set ℝ) (x₀ : ℝ) :

E

The kth coefficient of the Taylor polynomial.

Equations

taylor_coeff_within f k s x₀ = (↑(k.factorial))⁻¹ • iterated_deriv_within k f s x₀

noncomputable def taylor_within {E : Type u_2} [normed_add_comm_group E] [normed_space ℝ E] (f : ℝ → E) (n : ℕ) (s : set ℝ) (x₀ : ℝ) :

polynomial_module ℝ E

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

taylor_within f n s x₀ = (finset.range (n + 1)).sum (λ (k : ℕ), ⇑(polynomial_module.comp (polynomial.X - ⇑polynomial.C x₀)) (⇑(polynomial_module.single ℝ k) (taylor_coeff_within f k s x₀)))

noncomputable def taylor_within_eval {E : Type u_2} [normed_add_comm_group E] [normed_space ℝ 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

taylor_within_eval f n s x₀ x = ⇑(polynomial_module.eval x) (taylor_within f n s x₀)

theorem taylor_within_succ {E : Type u_2} [normed_add_comm_group E] [normed_space ℝ E] (f : ℝ → E) (n : ℕ) (s : set ℝ) (x₀ : ℝ) :

taylor_within f (n + 1) s x₀ = taylor_within f n s x₀ + ⇑(polynomial_module.comp (polynomial.X - ⇑polynomial.C x₀)) (⇑(polynomial_module.single ℝ (n + 1)) (taylor_coeff_within f (n + 1) s x₀))

@[simp]

theorem taylor_within_eval_succ {E : Type u_2} [normed_add_comm_group E] [normed_space ℝ E] (f : ℝ → E) (n : ℕ) (s : set ℝ) (x₀ x : ℝ) :

taylor_within_eval f (n + 1) s x₀ x = taylor_within_eval f n 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} [normed_add_comm_group E] [normed_space ℝ E] (f : ℝ → E) (s : set ℝ) (x₀ x : ℝ) :

taylor_within_eval f 0 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} [normed_add_comm_group E] [normed_space ℝ E] (f : ℝ → E) (n : ℕ) (s : set ℝ) (x₀ : ℝ) :

taylor_within_eval 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} [normed_add_comm_group E] [normed_space ℝ E] (f : ℝ → E) (n : ℕ) (s : set ℝ) (x₀ x : ℝ) :

taylor_within_eval f n s x₀ x = (finset.range (n + 1)).sum (λ (k : ℕ), ((↑(k.factorial))⁻¹ * (x - x₀) ^ k) • iterated_deriv_within k f s x₀)

theorem continuous_on_taylor_within_eval {E : Type u_2} [normed_add_comm_group E] [normed_space ℝ E] {f : ℝ → E} {x : ℝ} {n : ℕ} {s : set ℝ} (hs : unique_diff_on ℝ s) (hf : cont_diff_on ℝ ↑n f s) :

continuous_on (λ (t : ℝ), taylor_within_eval f n 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} [normed_add_comm_group E] [normed_space ℝ E] {f : ℝ → E} {x y : ℝ} {k : ℕ} {s t : set ℝ} (ht : unique_diff_within_at ℝ t y) (hs : s ∈ nhds_within y t) (hf : differentiable_within_at ℝ (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} [normed_add_comm_group E] [normed_space ℝ E] {f : ℝ → E} {x y : ℝ} {n : ℕ} {s s' : set ℝ} (hs'_unique : unique_diff_within_at ℝ s' y) (hs_unique : unique_diff_on ℝ s) (hs' : s' ∈ nhds_within y s) (hy : y ∈ s') (h : s' ⊆ s) (hf : cont_diff_on ℝ ↑n f s) (hf' : differentiable_within_at ℝ (iterated_deriv_within n f s) s y) :

has_deriv_within_at (λ (t : ℝ), taylor_within_eval f n 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} [normed_add_comm_group E] [normed_space ℝ E] {f : ℝ → E} {a b t : ℝ} (x : ℝ) {n : ℕ} (hx : a < b) (ht : t ∈ set.Ioo a b) (hf : cont_diff_on ℝ ↑n f (set.Icc a b)) (hf' : differentiable_on ℝ (iterated_deriv_within n f (set.Icc a b)) (set.Ioo a b)) :

has_deriv_at (λ (y : ℝ), taylor_within_eval f n (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} [normed_add_comm_group E] [normed_space ℝ E] {f : ℝ → E} {a b t : ℝ} (x : ℝ) {n : ℕ} (hx : a < b) (ht : t ∈ set.Icc a b) (hf : cont_diff_on ℝ ↑n f (set.Icc a b)) (hf' : differentiable_on ℝ (iterated_deriv_within n f (set.Icc a b)) (set.Icc a b)) :

has_deriv_within_at (λ (y : ℝ), taylor_within_eval f n (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 : cont_diff_on ℝ ↑n f (set.Icc x₀ x)) (hf' : differentiable_on ℝ (iterated_deriv_within n f (set.Icc x₀ x)) (set.Ioo x₀ x)) (gcont : continuous_on g (set.Icc x₀ x)) (gdiff : ∀ (x_1 : ℝ), x_1 ∈ set.Ioo x₀ x → has_deriv_at g (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 - taylor_within_eval f n (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 : cont_diff_on ℝ ↑n f (set.Icc x₀ x)) (hf' : differentiable_on ℝ (iterated_deriv_within n f (set.Icc x₀ x)) (set.Ioo x₀ x)) :

∃ (x' : ℝ) (hx' : x' ∈ set.Ioo x₀ x), f x - taylor_within_eval f n (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 : cont_diff_on ℝ ↑n f (set.Icc x₀ x)) (hf' : differentiable_on ℝ (iterated_deriv_within n f (set.Icc x₀ x)) (set.Ioo x₀ x)) :

∃ (x' : ℝ) (hx' : x' ∈ set.Ioo x₀ x), f x - taylor_within_eval f n (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} [normed_add_comm_group E] [normed_space ℝ E] {f : ℝ → E} {a b C x : ℝ} {n : ℕ} (hab : a ≤ b) (hf : cont_diff_on ℝ (↑n + 1) f (set.Icc a b)) (hx : x ∈ set.Icc a b) (hC : ∀ (y : ℝ), y ∈ set.Icc a b → ‖iterated_deriv_within (n + 1) f (set.Icc a b) y‖ ≤ C) :

‖f x - taylor_within_eval 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} [normed_add_comm_group E] [normed_space ℝ E] {f : ℝ → E} {a b : ℝ} {n : ℕ} (hab : a ≤ b) (hf : cont_diff_on ℝ (↑n + 1) f (set.Icc a b)) :

∃ (C : ℝ), ∀ (x : ℝ), x ∈ set.Icc a b → ‖f x - taylor_within_eval 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).