The Lean 4 theorem `wallHam_nonneg_form` in the `ChapterWallEsaSemibounded` chapter of the timepiece formalization
ProvedBookProof.WallEsaSemibounded.wallHam_nonneg_formtimepiece
The Lean 4 theorem wallHam_nonneg_form in the ChapterWallEsaSemibounded chapter of the timepiece formalization.
Preamble
-- Generated from ChapterWallEsaSemibounded.lean — theorem BookProof.WallEsaSemibounded.wallHam_nonneg_form
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.wallHam_nonneg_form (V : ℝ → ℝ)
(hV : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) V) (hVnn : ∀ x, 0 ≤ V x) :
SemiboundedBelowOn (ccDomain ℝ) (wallHam V hV) 0 := by sorrySource