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

Proved

BookProof.ScalaronWallEsa.kinCcR_symmetricOn

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

timepiece

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

Preamble

-- Generated from ChapterScalaronWallEsa.lean — theorem BookProof.ScalaronWallEsa.kinCcR_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.kinCcR_symmetricOn : SymmetricOn (ccDomain ℝ) kinCcR := by sorry

Source

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

View graph