The Lean 4 theorem `two_le_Vexp` in the `ChapterSchrodingerCutoffEsa` chapter of the timepiece formalization

-- Generated from ChapterSchrodingerCutoffEsa.lean — theorem BookProof.SchrodingerCutoff.two_le_Vexp
import Mathlib
import Definitions.Def_ChapterSchrodingerCutoffEsa
open BookProof.SchrodingerCutoff



open MeasureTheory Filter Complex

theorem BookProof.SchrodingerCutoff.two_le_Vexp (x : ℝ) : 2 ≤ Vexp x := by sorry