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

TODO

• the integral form of the remainder
• 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_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.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_1 ∈ Set.Ioo x₀ x, HasDerivAt g (g' x_1) x_1) (g'_ne : ∀ x_1 ∈ Set.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_lagrange_iteratedDeriv {f : ℝ → ℝ} {x x₀ : ℝ} {n : ℕ} (hx : x₀ < x) (hf : ContDiffOn ℝ (↑n + 1) f (Set.Icc x₀ x)) : ∃ x' ∈ Set.Ioo x₀ x, f x - taylorWithinEval f n (Set.Icc 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.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 : ∀ 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).