The Lean 4 theorem `wallHam_symmetricOn` in the `ChapterScalaronWallEsa` chapter of the timepiece formalization

Proved

BookProof.ScalaronWallEsa.wallHam_symmetricOn

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

timepiece

The Lean 4 theorem wallHam_symmetricOn in the ChapterScalaronWallEsa chapter of the timepiece formalization.

Preamble

-- Generated from ChapterScalaronWallEsa.lean — theorem BookProof.ScalaronWallEsa.wallHam_symmetricOn
import Mathlib
import Definitions.Def_ChapterScalaronWallEsa
open BookProof.ScalaronWallEsa












open MeasureTheory SchwartzMap Set
open BookProof.FarisLavine BookProof.StrichartzWave BookProof.ScalaronEsa
open BookProof.Starobinsky BookProof.StoneBridge BookProof.EsaClosure
open BookProof.ChapterStoneResolvent
open BookProof.WeakSecondDeriv

noncomputable section

Formal statement

theorem BookProof.ScalaronWallEsa.wallHam_symmetricOn (V : ℝ → ℝ) (hV : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) V) :
    SymmetricOn (ccDomain ℝ) (wallHam V hV) := by sorry

Source

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

View graph