Prove2Me

`BookProof.ChapterCayleySpectralModel.cfcHom_opSymbol` (y : H) : cfcHom (isStarNormal_cayleyCLM T) (opSymbol T) y = T.op (T.res (-1) y)

Proved
BookProof.ChapterCayleySpectralModel.cfcHom_opSymbol

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterCayleySpectralModel.

BookProof.ChapterCayleySpectralModel.cfcHom_opSymbol (y : H) : cfcHom (isStarNormal_cayleyCLM T) (opSymbol T) y = T.op (T.res (-1) y)

Formalization note: Lean 4 identifier BookProof.ChapterCayleySpectralModel.cfcHom_opSymbol.

Preamble
-- Generated from ChapterCayleySpectralModel.lean — theorem BookProof.ChapterCayleySpectralModel.cfcHom_opSymbol
import Definitions.Def_ChapterUnitaryTransport
import Definitions.Def_ChapterSirkTrotterKato
import Definitions.Def_ChapterAbelianGelfandModel
import Definitions.Def_ChapterSpectralMultiplication
import Mathlib
import Definitions.Def_ChapterCayleySpectralModel
import Definitions.Def_ChapterCayleyTransform
import Definitions.Def_ChapterStoneResolvent
open BookProof.ChapterCayleyTransform
open BookProof.ChapterCayleySpectralModel


open scoped InnerProductSpace
open MeasureTheory


open BookProof.ChapterUnitaryTransport BookProof.ChapterStoneResolvent
open BookProof.ChapterCayleyTransform BookProof.ChapterAbelianGelfandModel
open BookProof.ChapterSpectralMultiplication

variable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
variable (T : UnboundedSelfAdjoint H)
Formal statement
theorem BookProof.ChapterCayleySpectralModel.cfcHom_opSymbol (y : H) :
    cfcHom (isStarNormal_cayleyCLM T) (opSymbol T) y = T.op (T.res (-1) y) := by sorry

View graph