# 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

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

The `k`th coefficient of the Taylor polynomial.

Equations

- taylorCoeffWithin f k s x₀ = (↑k.factorial)⁻¹ • iteratedDerivWithin k f s x₀

Instances For

source
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`.

Equations

- taylorWithin f n s x₀ = ∑ k ∈ Finset.range (n + 1), (PolynomialModule.comp (Polynomial.X - Polynomial.C x₀)) ((PolynomialModule.single ℝ k) (taylorCoeffWithin f k s x₀))

Instances For

source
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

- taylorWithinEval f n s x₀ x = (PolynomialModule.eval x) (taylorWithin f n s x₀)

Instances For

source
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₀))
source
@[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₀
source
@[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`.

source
@[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`.

source
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₀
source
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₀`.

source
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.

source
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
source
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

source
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

source
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

source
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`.

source
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.

source
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.

source
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 #

source
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$.

source
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.

source
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.

source
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.

source
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`.

source
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)`.