Taylor-like theorems

TheoremTaylor's theorem with integral form for remainder (Taylor-like theorems)#

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.

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

Sources

• Mathlib documentation: taylor_integral_remainder_of_absolutelyContinuous
• Source of taylor_integral_remainder_of_absolutelyContinuous in Mathlib/Analysis/Calculus/Taylor.lean
• Mathlib undergraduate list: Single Variable Real Analysis › Taylor-like theorems

Mathlibtaylor_integral_remainder_of_absolutelyContinuous

Uses 9

Statement usesBochner integral · Carathéodory's theorem (measure theory) · Lebesgue measure (Measures and integral calculus) · Polynomial in one indeterminate · Radius of convergence

Proof usesDifferentiability of integrals with respect to parameters · Differentiable function between normed vector spaces · Differentials (linear tangent functions) · Polynomial functions

TheoremTaylor's theorem with Lagrange form for remainder#

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.

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

Freek Wiedijk's list (no. 35) also cites taylor_mean_remainder_cauchy, map_add_eq_sum_add_integral_iteratedFDeriv.

The 1000+ list (Q1137206) also cites taylor_mean_remainder_cauchy.

Sources

• Mathlib documentation: taylor_mean_remainder_lagrange
• Source of taylor_mean_remainder_lagrange in Mathlib/Analysis/Calculus/Taylor.lean
• Mathlib undergraduate list: Single Variable Real Analysis › Taylor-like theorems
• Freek Wiedijk's 100 theorems, no. 35
• 1000+ theorems list: Q1137206
• 1000+ theorems project: Q1137206
• Wikipedia: Taylor's theorem
• Wikidata: Q1137206

Mathlibtaylor_mean_remainder_lagrange

Uses 16

Statement usesHolomorphic functions · Infinite sum · Inner product space, over \(R\) or \(C\) · Norm of a continuous linear map · Polynomial in one indeterminate · Radius of convergence

Proof usesCharacteristic zero · Closure · Cluster point · Derivative at a point · Field \(\R\) of real numbers · Generating sets · Ordered ring · Polynomial functions · Topological ring · Topology on a normed vector space

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.