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

• taylorCoeffWithin: the Taylor coefficient using iteratedDerivWithin
• taylorWithin: the Taylor polynomial using iteratedDerivWithin

Main statements

• taylor_tendsto: Taylor's theorem as a limit
• taylor_isLittleO: Taylor's theorem using little-o notation
• 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
• taylor_integral_remainder_of_absolutelyContinuous, taylor_integral_remainder: Taylor's theorem with the integral form of the remainder

TODO

• Generalization to higher dimensions

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.

noncomputable def taylorWithin {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ℝ → E) (n : ℕ) (s : Set ℝ) (x₀ : ℝ) : PolynomialModule ℝ 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.

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

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 = ∑ k ∈ Finset.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 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 s' : Set ℝ} (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

theorem hasDerivAt_taylorWithinEval_succ {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {x₀ x : ℝ} {s : Set ℝ} (f : ℝ → E) (n : ℕ) : HasDerivAt (taylorWithinEval f (n + 1) s x₀) (taylorWithinEval (derivWithin f s) n s x₀ x) x

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

theorem taylor_isLittleO {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {x₀ : ℝ} {n : ℕ} {s : Set ℝ} (hs : Convex ℝ s) (hx₀s : x₀ ∈ s) (hf : ContDiffOn ℝ (↑n) f s) : (fun (x : ℝ) => f x - taylorWithinEval f n s x₀ x) =o[nhdsWithin x₀ s] fun (x : ℝ) => (x - x₀) ^ n

Taylor's theorem using little-o notation.

theorem taylor_isLittleO_univ {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {x₀ : ℝ} {n : ℕ} (hf : ContDiff ℝ (↑n) f) : (fun (x : ℝ) => f x - taylorWithinEval f n Set.univ x₀ x) =o[nhds x₀] fun (x : ℝ) => (x - x₀) ^ n

theorem taylor_tendsto {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {x₀ : ℝ} {n : ℕ} {s : Set ℝ} (hs : Convex ℝ s) (hx₀s : x₀ ∈ s) (hf : ContDiffOn ℝ (↑n) f s) : Filter.Tendsto (fun (x : ℝ) => ((x - x₀) ^ n)⁻¹ • (f x - taylorWithinEval f n s x₀ x)) (nhdsWithin x₀ s) (nhds 0)

Taylor's theorem as a limit.

theorem Real.taylor_tendsto {f : ℝ → ℝ} {x₀ : ℝ} {n : ℕ} {s : Set ℝ} (hs : Convex ℝ s) (hx₀s : x₀ ∈ s) (hf : ContDiffOn ℝ (↑n) f s) : Filter.Tendsto (fun (x : ℝ) => (f x - taylorWithinEval f n s x₀ x) / (x - x₀) ^ n) (nhdsWithin x₀ s) (nhds 0)

Taylor's theorem as a limit.

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.uIcc x₀ x)) (hf' : DifferentiableOn ℝ (iteratedDerivWithin n f (Set.uIcc x₀ x)) (Set.uIoo x₀ x)) (gcont : ContinuousOn g (Set.uIcc x₀ x)) (gdiff : ∀ x_1 ∈ Set.uIoo x₀ x, HasDerivAt g (g' x_1) x_1) (g'_ne : ∀ 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$.

theorem taylor_mean_remainder_lagrange {f : ℝ → ℝ} {x x₀ : ℝ} {n : ℕ} (hx : x₀ ≠ x) (hf : ContDiffOn ℝ (↑n) f (Set.uIcc x₀ x)) (hf' : 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.

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

A corollary of Taylor's theorem with the Lagrange form of the remainder.

theorem taylor_mean_remainder_cauchy {f : ℝ → ℝ} {x x₀ : ℝ} {n : ℕ} (hx : x₀ ≠ x) (hf : ContDiffOn ℝ (↑n) f (Set.uIcc x₀ x)) (hf' : 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 / ↑n.factorial * (x - x₀)

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

We assume that f is n-times continuously differentiable on 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 (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 : ∀ y ∈ Set.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 : ℝ), ∀ x ∈ Set.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).

theorem taylor_integral_remainder_aux {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : ℝ → F} {x x₀ : ℝ} {n : ℕ} (hf : ∀ k ≤ n, have u := fun (t : ℝ) => (x - t) ^ k / ↑k.factorial; have v := fun (t : ℝ) => iteratedDerivWithin k f (Set.uIcc x₀ x) t; ∫ (t : ℝ) in x₀..x, u t • deriv v t = u x • v x - u x₀ • v x₀ - ∫ (t : ℝ) in x₀..x, deriv u t • v t) : f x - taylorWithinEval f n (Set.uIcc x₀ x) x₀ x = ∫ (t : ℝ) in x₀..x, ((x - t) ^ n / ↑n.factorial) • iteratedDerivWithin (n + 1) f (Set.uIcc x₀ x) t

Taylor's theorem with the Integral form of the remainder. This is an auxiliary theorem which is used to prove the two useful versions taylor_integral_remainder_of_absolutelyContinuous and taylor_integral_remainder.

We assume that for any k ≤ n, the following equation on integration by parts hold: $$\int_{x_0}^x \frac{f^{(k+1)}(t) (x - t)^k}{k!} = \frac{f^{(k)}(t) (x - t)^k}{k!} |_{x_0}^x -\int_{x_0}^x \frac{f^{(k)}(t) (x - t)^{k-1}}{(k-1)!}.$$ Then $$f(x) - (P_n f)(x₀, x) = \int_{x_0}^x \frac{f^{(n+1)}(t) (x - t)^n}{n!} dt,$$ where $P_n f$ denotes the Taylor polynomial of degree $n$ and $f^{(n+1)}$ is the $n+1$-th iterated derivative.

theorem taylor_integral_remainder_of_absolutelyContinuous {f : ℝ → ℝ} {x x₀ : ℝ} {n : ℕ} (hf₁ : ContDiffOn ℝ (↑n) f (Set.uIcc x₀ x)) (hf₂ : AbsolutelyContinuousOnInterval (iteratedDerivWithin n f (Set.uIcc x₀ x)) x₀ x) : f x - taylorWithinEval f n (Set.uIcc x₀ x) x₀ x = ∫ (t : ℝ) in x₀..x, (x - t) ^ n / ↑n.factorial * iteratedDerivWithin (n + 1) f (Set.uIcc x₀ x) t

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

We assume that f is n-times continuously differentiable on the closed set uIcc x₀ x and its n-th derivative is absolutely continuous on uIcc x₀ x. Then $$f(x) - (P_n f)(x₀, x) = \int_{x_0}^x \frac{f^{(n+1)}(t) (x - t)^n}{n!} dt,$$ where $P_n f$ denotes the Taylor polynomial of degree $n$ and $f^{(n+1)}$ is the $n+1$-th iterated derivative.

theorem taylor_integral_remainder {F : Type u_3} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {f : ℝ → F} {x x₀ : ℝ} {n : ℕ} (hf : ContDiffOn ℝ (↑(n + 1)) f (Set.uIcc x₀ x)) : f x - taylorWithinEval f n (Set.uIcc x₀ x) x₀ x = ∫ (t : ℝ) in x₀..x, ((x - t) ^ n / ↑n.factorial) • iteratedDerivWithin (n + 1) f (Set.uIcc x₀ x) t

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

We assume that f is n+1-times continuously differentiable on the closed set uIcc x₀ x. Then $$f(x) - (P_n f)(x₀, x) = \int_{x_0}^x \frac{f^{(n+1)}(t) (x - t)^n}{n!} dt,$$ where $P_n f$ denotes the Taylor polynomial of degree $n$ and $f^{(n+1)}$ is the $n+1$-th iterated derivative.