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

## 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 taylorCoeffWithin {E : Type u_2} [] (f : E) (k : ) (s : ) (x₀ : ) :
E

The kth coefficient of the Taylor polynomial.

Equations
Instances For
noncomputable def taylorWithin {E : Type u_2} [] (f : E) (n : ) (s : ) (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
Instances For
noncomputable def taylorWithinEval {E : Type u_2} [] (f : E) (n : ) (s : ) (x₀ : ) (x : ) :
E

The Taylor polynomial with derivatives inside of a set s considered as a function ℝ → E

Equations
Instances For
theorem taylorWithin_succ {E : Type u_2} [] (f : E) (n : ) (s : ) (x₀ : ) :
taylorWithin f (n + 1) s x₀ = taylorWithin f n s x₀ + (PolynomialModule.comp (Polynomial.X - Polynomial.C x₀)) (() (taylorCoeffWithin f (n + 1) s x₀))
@[simp]
theorem taylorWithinEval_succ {E : Type u_2} [] (f : E) (n : ) (s : ) (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} [] (f : E) (s : ) (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} [] (f : E) (n : ) (s : ) (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} [] (f : E) (n : ) (s : ) (x₀ : ) (x : ) :
taylorWithinEval f n s x₀ x = kFinset.range (n + 1), ((k.factorial)⁻¹ * (x - x₀) ^ k) iteratedDerivWithin k f s x₀
theorem continuousOn_taylorWithinEval {E : Type u_2} [] {f : E} {x : } {n : } {s : } (hs : ) (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} [] {f : E} {x : } {y : } {k : } {s : } {t : } (ht : ) (hs : s ) (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} [] {f : E} {x : } {y : } {n : } {s : } {s' : } (hs'_unique : ) (hs_unique : ) (hs' : s' ) (hy : y s') (h : s' s) (hf : ContDiffOn (n) f s) (hf' : ) :
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} [] {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} [] {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

### 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_1Set.Ioo x₀ x, HasDerivAt g (g' x_1) x_1) (g'_ne : x_1Set.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_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} [] {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 : ySet.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} [] {f : E} {a : } {b : } {n : } (hab : a b) (hf : ContDiffOn (n + 1) f (Set.Icc a b)) :
∃ (C : ), xSet.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).