OAI/Analysis/AffineBernstein/QuadraticIntegration.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.AffineBernstein.quadratic_of_third_fderiv_zero line 18

   Source documentation

   The last, purely analytic step of the rescaling argument: a C³ function with zero third derivative everywhere is exactly its quadratic Taylor polynomial.

   theorem quadratic_of_third_fderiv_zero (f : E → ℝ) (hf : ContDiff ℝ 3 f)
       (hthird : ∀ x, fderiv ℝ (fderiv ℝ (fderiv ℝ f)) x = 0) :
       ∀ x, f x = (1 / 2 : ℝ) * (fderiv ℝ (fderiv ℝ f) 0 x x) +
         fderiv ℝ f 0 x + f 0 := by
   …