Prove2Me

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

Proved
BookProof.SchrodingerCutoff.deriv_chi_continuous

by leonardopedro · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

timepiece

The Lean 4 theorem deriv_chi_continuous in the ChapterSchrodingerCutoffEsa chapter of the timepiece formalization.

Preamble
-- Generated from ChapterSchrodingerCutoffEsa.lean — theorem BookProof.SchrodingerCutoff.deriv_chi_continuous
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.deriv_chi_continuous : Continuous (deriv chi) := by sorry
Source
https://github.com/leonardopedro/timepiece/blob/61595bc/BookProof/ChapterSchrodingerCutoffEsa.lean

View graph