`BookProof.ChapterStoneSeparable.eq_stoneU_of_hasDerivAt` (T : UnboundedSelfAdjoint H) (G : WeakMeasurableUnitaryGroup H) (h : ∀ x : T.domain, HasDerivAt (fun t : ℝ => G.U t (x : H

Proved

BookProof.ChapterStoneSeparable.eq_stoneU_of_hasDerivAt

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterStoneSeparable.

BookProof.ChapterStoneSeparable.eq_stoneU_of_hasDerivAt (T : UnboundedSelfAdjoint H) (G : WeakMeasurableUnitaryGroup H) (h : ∀ x : T.domain, HasDerivAt (fun t : ℝ => G.U t (x : H)) ((-Complex.I) • T.op x) 0) (t : ℝ) : G.U t = T.stoneU t

Formalization note: Lean 4 identifier BookProof.ChapterStoneSeparable.eq_stoneU_of_hasDerivAt.

Preamble

-- Generated from ChapterStoneSeparable.lean — theorem BookProof.ChapterStoneSeparable.eq_stoneU_of_hasDerivAt
import Definitions.Def_ChapterSirkTrotterKato
import Mathlib
import Definitions.Def_ChapterStoneSeparable
import Definitions.Def_ChapterStoneConverse
import Definitions.Def_ChapterStoneMeasurable
import Definitions.Def_ChapterStoneResolvent
import Definitions.Def_ChapterStoneUnitary
open BookProof.ChapterStoneMeasurable
open BookProof.ChapterStoneMeasurable
open BookProof.ChapterStoneSeparable


open scoped InnerProductSpace
open Filter Topology


open BookProof.ChapterStoneResolvent BookProof.ChapterStoneMeasurable

variable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
  [TopologicalSpace.SeparableSpace H]

Formal statement

theorem BookProof.ChapterStoneSeparable.eq_stoneU_of_hasDerivAt (T : UnboundedSelfAdjoint H) (G : WeakMeasurableUnitaryGroup H)
    (h : ∀ x : T.domain, HasDerivAt (fun t : ℝ => G.U t (x : H)) ((-Complex.I) • T.op x) 0)
    (t : ℝ) : G.U t = T.stoneU t := by sorry

View graph