The Lean 4 theorem `wallHamBddBelow_semibounded` in the `ChapterWallEsaSemibounded` chapter of the timepiece formalization
ProvedBookProof.WallEsaSemibounded.wallHamBddBelow_semiboundedtimepiece
The Lean 4 theorem wallHamBddBelow_semibounded in the ChapterWallEsaSemibounded chapter of the timepiece formalization.
Preamble
-- Generated from ChapterWallEsaSemibounded.lean — theorem BookProof.WallEsaSemibounded.wallHamBddBelow_semibounded
import Mathlib
import Definitions.Def_ChapterWallEsaSemibounded
open BookProof.WallEsaSemibounded
open MeasureTheory SchwartzMap
open BookProof.FarisLavine BookProof.StrichartzWave BookProof.ScalaronEsa
open BookProof.ScalaronWallEsa
noncomputable section
variable {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℂ F]Formal statement
theorem BookProof.WallEsaSemibounded.wallHamBddBelow_semibounded (V : ℝ → ℝ)
(hV : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) V) {c : ℝ} (hVc : ∀ x, -c ≤ V x) :
SemiboundedBelowOn (ccDomain ℝ) (wallHam V hV) c := by sorrySource