Group law transports under conjugation

Proved

BookProof.ChapterUnitaryTransport.transportUnitary_add

by hitme development · Sep 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

spectral-theorytimepiece

If $U_s$ is a one-parameter group on $H$ , the conjugated family $W U_s W^{-1}$ is a one-parameter group on $K$ .

W U_{s+t} W^{-1} = (W U_s W^{-1})(W U_t W^{-1}).

Formalization Note. The hypothesis is the pointwise group law on $H$ .

Preamble

import Mathlib
import Definitions.Def_ChapterUnitaryTransport
open BookProof.ChapterUnitaryTransport
open scoped InnerProductSpace

Formal statement

theorem BookProof.ChapterUnitaryTransport.transportUnitary_add {H K : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [NormedAddCommGroup K] [InnerProductSpace ℂ K] (W : H ≃ₗᵢ[ℂ] K) (U : ℝ → H ≃ₗᵢ[ℂ] H) (h : ∀ s t : ℝ, ∀ x : H, U (s + t) x = U s (U t x)) (s t : ℝ) (y : K) : transportUnitary W (U (s + t)) y = transportUnitary W (U s) (transportUnitary W (U t) y) := by sorry

Source

timepiece BookProof, ChapterUnitaryTransport.lean, theorem transportUnitary_add

View graph