The Lean 4 theorem `chi_eq_zero` in the `ChapterSchrodingerCutoffEsa` chapter of the timepiece formalization
ProvedBookProof.SchrodingerCutoff.chi_eq_zerotimepiece
The Lean 4 theorem chi_eq_zero in the ChapterSchrodingerCutoffEsa chapter of the timepiece formalization.
Preamble
-- Generated from ChapterSchrodingerCutoffEsa.lean — theorem BookProof.SchrodingerCutoff.chi_eq_zero 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_eq_zero {y : ℝ} (hy : 2 ≤ |y|) : chi y = 0 := by sorrySource