(p : Polynomial ℝ) (x : ℝ) : HasDerivAt (gaussPoly p) (gaussPoly (gaussPolyDeriv p) x) x

-- Generated from ChapterQgHermiteCore.lean — theorem BookProof.QgHermiteCore.hasDerivAt_gaussPoly
import Mathlib
import Definitions.Def_ChapterQgHermiteCore
open BookProof.QgHermiteCore













open MeasureTheory Polynomial Filter Topology
open BookProof.HermiteCore BookProof.Starobinsky







variable {E : Type*} [NormedAddCommGroup E]

theorem BookProof.QgHermiteCore.hasDerivAt_gaussPoly (p : Polynomial ℝ) (x : ℝ) :
    HasDerivAt (gaussPoly p) (gaussPoly (gaussPolyDeriv p) x) x := by sorry