Physlib

PhyslibAlpha.ProbabilisticTheory.HilbertSpace.Unbounded.Flow.Stone

The unitary group of a self-adjoint operator

i. Overview

For a self-adjoint operator `T` with spectral measure `μ`, the unitary group `exp(i t T)` is the integral of `exp(i t λ)`. A vector `x` lies in the domain of `T` exactly when its orbit is differentiable at `0`, and then the derivative at time `t` is `i T exp(i t T) x`.

ii. Key results

- `expUnitaryGroup_strong_slope_tendsto` : the difference quotients of the orbit converge to `i T x`. - `expUnitaryGroup_hasDerivAt` : orbits of domain vectors are differentiable at every time. - `mem_domain_iff_expUnitaryGroup_hasDerivAt_zero` : the domain is the set of vectors with differentiable orbit. - `expUnitaryGroup_star` : `exp(i t T)⋆ = exp(-i t T)`.

6 declarations

theorem

The difference quotient of eitTxe^{itT}x tends to iTxiTx as t→0t \to 0

Let TT be a self-adjoint operator on a Hilbert space HH with an associated spectral measure μ\mu, and let U(t)=eitTU(t) = e^{itT} be the strongly continuous one-parameter unitary group defined by the spectral integral U(t)=∫Reitλ dμ(λ)U(t) = \int_{\mathbb{R}} e^{it\lambda} \, d\mu(\lambda). For any vector xx in the domain of TT, the difference quotient at t=0t=0 converges to iTxi T x as t→0t \to 0. That is, lim⁡t→0eitTx−xt=iTx, \lim_{t \to 0} \frac{e^{itT} x - x}{t} = i T x, where ii is the imaginary unit.

theorem

ddteitTx∣t=0=iTx\frac{d}{dt} e^{itT}x \big|_{t=0} = iTx for x∈dom(T)x \in \text{dom}(T)

Let TT be a self-adjoint operator on a Hilbert space HH with spectral measure μ\mu. Let U(t)=eitTU(t) = e^{itT} be the strongly continuous one-parameter unitary group defined by the spectral integral U(t)=∫Reitλ dμ(λ). U(t) = \int_{\mathbb{R}} e^{it\lambda} \, d\mu(\lambda). For any vector xx in the domain of TT, the orbit t↦U(t)xt \mapsto U(t)x is differentiable at t=0t = 0 with derivative iTxiTx, where ii denotes the imaginary unit.

theorem

The orbit t↦eitTxt \mapsto e^{itT}x is differentiable at any ss for x∈dom(T)x \in \text{dom}(T) with derivative eisT(iTx)e^{isT}(iTx)

Let HH be a Hilbert space and TT a self-adjoint operator on HH. Let U(t)=eitTU(t) = e^{itT} be the strongly continuous one-parameter unitary group generated by TT via the spectral theorem. For any vector xx in the domain of TT and any time s∈Rs \in \mathbb{R}, the map t↦U(t)xt \mapsto U(t)x is differentiable at t=st = s with derivative ddt∣t=seitTx=eisT(iTx). \frac{d}{dt} \bigg|_{t=s} e^{itT}x = e^{isT}(iTx).

theorem

x∈dom(T)x \in \text{dom}(T) iff the limit of eitTx−xt\frac{e^{itT}x - x}{t} exists as t→0t \to 0

Let HH be a Hilbert space and TT be a self-adjoint operator on HH with an associated spectral measure. Let U(t)=eitTU(t) = e^{itT} be the strongly continuous one-parameter unitary group defined by the spectral integral U(t)=∫Reitλ dμ(λ)U(t) = \int_{\mathbb{R}} e^{it\lambda} \, d\mu(\lambda). For any vector x∈Hx \in H, xx belongs to the domain of TT if and only if the limit of the difference quotient lim⁡t→0U(t)x−xt \lim_{t \to 0} \frac{U(t)x - x}{t} exists in HH.

theorem

x∈D(T)x \in \mathcal{D}(T) iff t↦eitTxt \mapsto e^{itT}x is differentiable at t=0t=0

Let HH be a Hilbert space and TT a self-adjoint operator with domain D(T)\mathcal{D}(T). Let U(t)=eitTU(t) = e^{itT} be the strongly continuous one-parameter unitary group defined by the spectral theorem as U(t)=∫Reitλ dμ(λ)U(t) = \int_{\mathbb{R}} e^{it\lambda} \, d\mu(\lambda). For any vector x∈Hx \in H, xx belongs to the domain D(T)\mathcal{D}(T) if and only if the orbit map t↦U(t)xt \mapsto U(t)x is differentiable at t=0t = 0.

theorem

(eitT)∗=e−itT(e^{itT})^* = e^{-itT}

Let TT be a self-adjoint operator on a Hilbert space and U(t)=eitTU(t) = e^{itT} be the associated one-parameter unitary group defined via the spectral theorem. For any t∈Rt \in \mathbb{R}, the adjoint of the operator U(t)U(t) is given by U(t)∗=U(−t)U(t)^* = U(-t), which can be expressed as (eitT)∗=e−itT(e^{itT})^* = e^{-itT}.