Taylors_Theorem
Disprovedcalculusproofwikitaylor-s-theorem
Every sufficiently differentiable function can be approximated by a polynomial via Taylor's theorem with remainder.
Preamble
import Mathlib.Analysis.Calculus.Taylor
Formal statement
theorem Taylors_Theorem {f : ℝ → ℝ} {a x : ℝ} {n : ℕ} (hf : ContDiff ℝ (n + 1) f) (hx : x ∈ Set.Icc (min a x) (max a x)) : ∃ c : ℝ, c ∈ Set.Ioo (min a x) (max a x) ∧ f x = ∑ k ∈ Finset.range (n + 1), (iteratedDeriv k f a / k.factorial) * (x - a) ^ k + (iteratedDeriv (n + 1) f c / (n + 1).factorial) * (x - a) ^ (n + 1) := by sorrySource