Prove2Me

`BookProof.ChapterStoneSeparable.stoneU_mulSA` (f : ℤ → ℝ) (t : ℝ) (psi : L2Z) : (mulSA f).stoneU t psi = phaseUnitary f (-t) psi

Proved
BookProof.ChapterStoneSeparable.stoneU_mulSA

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterStoneSeparable.

BookProof.ChapterStoneSeparable.stoneU_mulSA (f : ℤ → ℝ) (t : ℝ) (psi : L2Z) : (mulSA f).stoneU t psi = phaseUnitary f (-t) psi

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

Preamble
-- Generated from ChapterStoneSeparable.lean — theorem BookProof.ChapterStoneSeparable.stoneU_mulSA
import Definitions.Def_ChapterSirkTrotterKato
import Definitions.Def_ChapterStoneConverse
import Mathlib
import Definitions.Def_ChapterStoneSeparable
import Definitions.Def_ChapterContinuityUnitaryInfinite
import Definitions.Def_ChapterStoneUnitary
import Definitions.Def_ChapterUnboundedPosition
open BookProof.ChapterContinuityUnitaryInfinite
open BookProof.ChapterUnboundedPosition
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.stoneU_mulSA (f : ℤ → ℝ) (t : ℝ) (psi : L2Z) :
    (mulSA f).stoneU t psi = phaseUnitary f (-t) psi := by sorry

View graph