The Lean 4 theorem `domain_le_genDomain` in the `ChapterStoneTheorem` chapter of the timepiece formalization
ProvedBookProof.ChapterStoneResolvent.UnboundedSelfAdjoint.domain_le_genDomainformalizationtimepiece
Formal statement of BookProof.ChapterStoneResolvent.UnboundedSelfAdjoint.domain_le_genDomain from the timepiece Lean 4 formalization: the domain of a self-adjoint operator is contained in the domain of the generator of its unitary group.
Preamble
-- Generated from ChapterStoneTheorem.lean — theorem BookProof.ChapterStoneResolvent.UnboundedSelfAdjoint.domain_le_genDomain
import Mathlib
import Definitions.Def_ChapterStoneTheorem
import Definitions.Def_ChapterStoneConverse
import Definitions.Def_ChapterStoneResolvent
import Definitions.Def_ChapterSirkTrotterKato
open BookProof.ChapterStoneMeasurable
open BookProof.ChapterStoneMeasurable.WeakMeasurableUnitaryGroup
open BookProof.ChapterStoneResolvent
open scoped InnerProductSpace
variable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H]
variable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]Formal statement
theorem BookProof.ChapterStoneResolvent.UnboundedSelfAdjoint.domain_le_genDomain (T : UnboundedSelfAdjoint H) :
T.domain ≤ T.stoneGroup.genDomain := by sorrySource