Theorems · Theorem · global analysis

map_add_eq_sum_add_integral_iteratedFDeriv

• #35 of the 100 theorems: Taylor’s Theorem

∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ E]
  [inst_3 : NormedSpace ℝ F] {f : E → F} {x y : E} {n : ℕ} [CompleteSpace F],
  (∀ t ∈ Set.Icc 0 1, ContDiffAt ℝ (↑n + 1) f (x + t • y)) →
    f (x + y) =
      (∑ k ∈ Finset.range (n + 1), (↑k.factorial)⁻¹ • (iteratedFDeriv ℝ k f x) fun x => y) +
        (↑n.factorial)⁻¹ • ∫ (t : ℝ) in 0..1, (1 - t) ^ n • (iteratedFDeriv ℝ (n + 1) f (x + t • y)) fun x => y

Taylor's theorem with remainder in integral form. If f is n + 1 times continuously differentiable, then f (x + y) is given by ∑ k in 0..n, D^k f(x; y,..,y) / k! + 1/n! ∫ t in 0..1, (1 - t) ^ n • D^{n+1}f (x + t • y; y,..,y), where D^k f denotes the iterated derivative of f. In the case that n = 1, this is a reformulation of the fundamental theorem of calculus, namely f (x + y) = f x + ∫ t in 0..1, D f(x + t • y; y).

Defined in

Mathlib.Analysis.Calculus.TaylorIntegral

Cited by

0 results in Mathlib

Foundations

Depth 272 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedAddCommGroupNormedSpaceNormedSpaceCompleteSpace