Physlib

PhyslibAlpha.ProbabilisticTheory.HilbertSpace.Unbounded.Flow.StoneInvariance

The unitary group preserves the domain of its generator

i. Overview

For a self-adjoint operator `T` with spectral measure `μ`, the unitary group `exp(i t T)` preserves the domain of `T` and commutes with `T` there.

ii. Key results

  • `expUnitaryGroup_translate_mem` : `exp(i s T)` preserves the domain of `T`.
  • `expUnitaryGroup_translate` : `T` commutes with `exp(i s T)` on its domain.

3 declarations

theorem

The Group Property U(t)U(s)=U(t+s)U(t)U(s) = U(t+s) for the Unitary Group eitTe^{itT}

Let HH be a Hilbert space and TT be a self-adjoint operator. Let U(t)=eitTU(t) = e^{itT} denote the strongly continuous one-parameter unitary group generated by TT via the spectral theorem. For any vector x∈Hx \in H and any parameters s,t∈Rs, t \in \mathbb{R}, the group law holds: U(t)(U(s)x)=U(t+s)x. U(t)(U(s)x) = U(t+s)x.

theorem

eisTe^{isT} preserves the domain of TT

Let TT be a self-adjoint operator on a Hilbert space HH with domain dom⁡(T)\operatorname{dom}(T). For any vector x∈dom⁡(T)x \in \operatorname{dom}(T) and any scalar s∈Rs \in \mathbb{R}, the vector eisTxe^{isT}x (the image of xx under the strongly continuous unitary group generated by TT) also belongs to dom⁡(T)\operatorname{dom}(T).

theorem

TT Commutes with its Unitary Group eisTe^{isT} on dom⁡(T)\operatorname{dom}(T)

Let TT be a self-adjoint operator on a Hilbert space HH with domain dom⁡(T)\operatorname{dom}(T), and let eisTe^{isT} denote the strongly continuous one-parameter unitary group generated by TT. For any vector x∈dom⁡(T)x \in \operatorname{dom}(T) and any scalar s∈Rs \in \mathbb{R}, the image eisTxe^{isT}x lies in dom⁡(T)\operatorname{dom}(T) and the operator TT commutes with the unitary group such that: T(eisTx)=eisT(Tx). T(e^{isT}x) = e^{isT}(Tx).