The Lean 4 theorem `starobinskyEdgeHam_symmetricOn` in the `ChapterScalaronEdge` chapter of the timepiece formalization

Proved

BookProof.ScalaronEdge.starobinskyEdgeHam_symmetricOn

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

timepiece

The Lean 4 theorem starobinskyEdgeHam_symmetricOn in the ChapterScalaronEdge chapter of the timepiece formalization.

Preamble

-- Generated from ChapterScalaronEdge.lean — theorem BookProof.ScalaronEdge.starobinskyEdgeHam_symmetricOn
import Mathlib
import Definitions.Def_ChapterScalaronEdge
open BookProof.ScalaronEdge









open Complex Real MeasureTheory Function SchwartzMap ComplexOrder
open BookProof.Starobinsky
open BookProof.ScalaronWallEsa
open BookProof.ScalaronEsa
open BookProof.FarisLavine
open BookProof.WallEsaSemibounded
open BookProof.FriedrichsExtension
open BookProof.FriedrichsFormGap
open BookProof.YangMillsFriedrichs
open BookProof.HashimotoShiftInvert



variable (M alpha : ℝ)

Formal statement

theorem BookProof.ScalaronEdge.starobinskyEdgeHam_symmetricOn :
    SymmetricOn (ccDomain ℝ) (starobinskyEdgeHam M alpha) := by sorry

Source

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

View graph