`BookProof.ChapterStoneMeasurable.WeakMeasurableUnitaryGroup.inner_left_shift` (s t : ℝ) (x y : H) : ⟪ y, G.U s (G.U t x) ⟫_ℂ = ⟪ G.U (-s) y, G.U t x ⟫_ℂ

Proved

BookProof.ChapterStoneMeasurable.WeakMeasurableUnitaryGroup.inner_left_shift

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterStoneMeasurable.

BookProof.ChapterStoneMeasurable.WeakMeasurableUnitaryGroup.inner_left_shift (s t : ℝ) (x y : H) : ⟪ y, G.U s (G.U t x) ⟫_ℂ = ⟪ G.U (-s) y, G.U t x ⟫_ℂ

Formalization note: Lean 4 identifier BookProof.ChapterStoneMeasurable.WeakMeasurableUnitaryGroup.inner_left_shift.

Preamble

-- Generated from ChapterStoneMeasurable.lean — theorem BookProof.ChapterStoneMeasurable.WeakMeasurableUnitaryGroup.inner_left_shift
import Mathlib
import Definitions.Def_ChapterStoneMeasurable
import Definitions.Def_ChapterStoneConverse
open BookProof.ChapterStoneMeasurable
open BookProof.ChapterStoneMeasurable


open scoped InnerProductSpace
open Filter Topology MeasureTheory


variable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H]

variable (G : WeakMeasurableUnitaryGroup H)

Formal statement

theorem BookProof.ChapterStoneMeasurable.WeakMeasurableUnitaryGroup.inner_left_shift (s t : ℝ) (x y : H) :
    ⟪ y, G.U s (G.U t x) ⟫_ℂ = ⟪ G.U (-s) y, G.U t x ⟫_ℂ := by sorry

View graph