PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.Flow.StoneAPI

Public generator API for an unbounded spectral theorem

`Unbounded.Flow.Stone` proves the analytic limit statements for the unitary group attached to a domain-aware spectral theorem. This file packages the most useful interface theorem: a vector is in the generator domain exactly when its orbit is differentiable at time zero. The result is stated with an existential derivative so that it is independent of the sign convention chosen for the group; a companion theorem identifies the derivative as `Complex.I • T x`.

This is only packaging. The actual work is the square-moment argument and the maximal-integral operator equality proved in `Unbounded.Flow.Stone` and `UnboundedSpectralIntegral`.

3 declarations

theorem

The orbit $e^{itT}x$ is differentiable at $t=0$ with derivative $y$ iff $x \in \mathcal{D}(T)$ and $y = iTx$

#expUnitaryGroup_hasDerivAt_zero_iff

Let $H$ be a Hilbert space and $T$ a self-adjoint operator on $H$ with domain $\mathcal{D}(T)$ . Let $U(t) = e^{itT}$ be the strongly continuous one-parameter unitary group associated with $T$ via the spectral theorem. For any vectors $x, y \in H$ , the map $t \mapsto U(t)x$ is differentiable at $t = 0$ with derivative $y$ if and only if $x \in \mathcal{D}(T)$ and $y = iTx$ , where $i$ is the imaginary unit.

theorem

$x \in \mathcal{D}(T)$ if and only if $t \mapsto e^{itT}x$ is differentiable at $t = s$

#mem_domain_iff_expUnitaryGroup_hasDerivAt

Let $H$ be a Hilbert space and $T$ be a self-adjoint operator with domain $\mathcal{D}(T)$ . Let $U(t) = e^{itT}$ be the strongly continuous one-parameter unitary group generated by $T$ . For any vector $x \in H$ and any time $s \in \mathbb{R}$ , $x$ belongs to the domain $\mathcal{D}(T)$ if and only if the orbit map $t \mapsto U(t)x$ is differentiable at $t = s$ .

theorem

The derivative of the unitary orbit $e^{itT}x$ at time $s$ is $e^{isT}(iTx)$

#expUnitaryGroup_hasDerivAt_iff

Let $H$ be a Hilbert space and $T$ be a self-adjoint operator on $H$ . Let $U(t) = e^{itT}$ denote the strongly continuous one-parameter unitary group associated with $T$ . For any vectors $x, y \in H$ and any time $s \in \mathbb{R}$ , the orbit $t \mapsto U(t)x$ is differentiable at $t = s$ with derivative $y$ if and only if $x$ is in the domain of $T$ and $y = U(s)(iTx)$ .

PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.Flow.StoneAPI

Public generator API for an unbounded spectral theorem

The orbit eitTxe^{itT}xeitTx is differentiable at t=0t=0t=0 with derivative yyy iff x∈D(T)x \in \mathcal{D}(T)x∈D(T) and y=iTxy = iTxy=iTx

x∈D(T)x \in \mathcal{D}(T)x∈D(T) if and only if t↦eitTxt \mapsto e^{itT}xt↦eitTx is differentiable at t=st = st=s

The derivative of the unitary orbit eitTxe^{itT}xeitTx at time sss is eisT(iTx)e^{isT}(iTx)eisT(iTx)

The orbit $e^{itT}x$ is differentiable at $t=0$ with derivative $y$ iff $x \in \mathcal{D}(T)$ and $y = iTx$

$x \in \mathcal{D}(T)$ if and only if $t \mapsto e^{itT}x$ is differentiable at $t = s$

The derivative of the unitary orbit $e^{itT}x$ at time $s$ is $e^{isT}(iTx)$