The Lean 4 theorem `chi_nonneg` in the `ChapterSchrodingerCutoffEsa` chapter of the timepiece formalization
ProvedBookProof.SchrodingerCutoff.chi_nonnegtimepiece
The Lean 4 theorem chi_nonneg in the ChapterSchrodingerCutoffEsa chapter of the timepiece formalization.
Preamble
-- Generated from ChapterSchrodingerCutoffEsa.lean — theorem BookProof.SchrodingerCutoff.chi_nonneg import Mathlib import Definitions.Def_ChapterSchrodingerCutoffEsa import Definitions.Def_ChapterParityChirality open BookProof.ChapterParityChirality open BookProof.SchrodingerCutoff open MeasureTheory Filter Complex
Formal statement
theorem BookProof.SchrodingerCutoff.chi_nonneg (x : ℝ) : 0 ≤ chi x := by sorry
Source