(A : H →L[ℂ] H) (hA : IsSelfAdjoint A) (y : H) : (ofBounded A hA).resCLM 1 y = -(resolvent A Complex.I y)
ProvedBookProof.ChapterSirkTrotterKato.resCLM_ofBoundedsirkspectral-theorytimepiece
Lean 4 theorem BookProof.ChapterSirkTrotterKato.resCLM_ofBounded (module BookProof.ChapterSirkTrotterKato), source chapter BookProof/ChapterChapterSirkTrotterKato.lean.
Preamble
-- Generated from ChapterSirkTrotterKatoGalerkin.lean — theorem BookProof.ChapterSirkTrotterKato.resCLM_ofBounded
import Mathlib
import Definitions.Def_ChapterSirkTrotterKatoGalerkin
open BookProof.ChapterSirkTrotterKato
noncomputable section
open Filter Topology
open BookProof.ChapterStoneResolvent BookProof.ChapterUnitaryTransport
variable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]Formal statement
theorem BookProof.ChapterSirkTrotterKato.resCLM_ofBounded (A : H →L[ℂ] H) (hA : IsSelfAdjoint A) (y : H) :
(ofBounded A hA).resCLM 1 y = -(resolvent A Complex.I y) := by sorrySource