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

Proved

BookProof.SchrodingerCutoff.chi_contDiff

by leonardopedro · Sep 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

timepiece

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

Preamble

-- Generated from ChapterSchrodingerCutoffEsa.lean — theorem BookProof.SchrodingerCutoff.chi_contDiff
import Mathlib
import Definitions.Def_ChapterSchrodingerCutoffEsa
open BookProof.SchrodingerCutoff



open MeasureTheory Filter Complex

Formal statement

theorem BookProof.SchrodingerCutoff.chi_contDiff : ContDiff ℝ 2 chi := by sorry

Source

https://github.com/leonardopedro/timepiece/blob/61595bc/BookProof/ChapterSchrodingerCutoffEsa.lean

View graph