(M alpha : ℝ) (hM : 0 < M) : ExpBounded (starobinskyV M alpha)

-- Generated from ChapterQgHermiteCore.lean — theorem BookProof.QgHermiteCore.expBounded_starobinskyV
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.expBounded_starobinskyV (M alpha : ℝ) (hM : 0 < M) :
    ExpBounded (starobinskyV M alpha) := by sorry