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

-- Generated from ChapterSchrodingerCutoffEsa.lean — theorem BookProof.SchrodingerCutoff.exists_deriv_chi_bound
import Mathlib
import Definitions.Def_ChapterSchrodingerCutoffEsa
import Definitions.Def_ChapterParityChirality
open BookProof.ChapterParityChirality
open BookProof.SchrodingerCutoff



open MeasureTheory Filter Complex

theorem BookProof.SchrodingerCutoff.exists_deriv_chi_bound : ∃ C : ℝ, 0 < C ∧ ∀ y, |deriv chi y| ≤ C := by sorry