Taylor's formula with an integral remainder in higher dimensions

In this file we prove Taylor's formula with the remainder term in integral form.

• map_add_eq_sum_add_integral_iteratedFDeriv: version for higher dimensions with iteratedFDeriv

TODO: add a version that assumes ContDiffOn f (closedBall x (‖y‖))

theorem DifferentiableAt.deriv_comp_add_smul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] {f : E → F} {x y : E} {t : 𝕜} (hf : DifferentiableAt 𝕜 f (x + t • y)) : deriv (fun (s : 𝕜) => f (x + s • y)) t = (fderiv 𝕜 f (x + t • y)) y

theorem ContDiffAt.deriv_fderiv_add_smul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedAddCommGroup F] [NontriviallyNormedField 𝕜] [NormedSpace 𝕜 E] [NormedSpace 𝕜 F] {f : E → F} {x y : E} {t : 𝕜} {n : ℕ} (hf : ContDiffAt 𝕜 (↑n + 1) f (x + t • y)) : deriv (fun (s : 𝕜) => (iteratedFDeriv 𝕜 n f (x + s • y)) fun (x : Fin n) => y) t = (iteratedFDeriv 𝕜 (n + 1) f (x + t • y)) fun (x : Fin (n + 1)) => y

theorem map_add_eq_sum_add_integral_iteratedFDeriv {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedSpace ℝ E] [NormedSpace ℝ F] {f : E → F} {x y : E} {n : ℕ} [CompleteSpace F] (hf : ∀ 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 : Fin k) => y) + (↑n.factorial)⁻¹ • ∫ (t : ℝ) in 0..1, (1 - t) ^ n • (iteratedFDeriv ℝ (n + 1) f (x + t • y)) fun (x : Fin (n + 1)) => 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).