PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.StoneUnitaryGroup

For a given real parameter $t \in \mathbb{R}$, this is the complex-valued function of a real variable $x \in \mathbb{R}$ defined by $x \mapsto e^{itx}$, where $i$ is the imaginary unit.

For any real number $t \in \mathbb{R}$, the complex-valued function $x \mapsto e^{itx}$ is measurable.

For any real number $t \in \mathbb{R}$, there exists a constant $C$ such that for all $x \in \mathbb{R}$, the magnitude of the exponential function $|e^{itx}| \leq C$.

For any real number $t$, the complex-valued function $x \mapsto e^{itx}$ has a modulus of 1 for all $x \in \mathbb{R}$. That is, $|e^{itx}| = 1$.

For any real number $t \in \mathbb{R}$, the function $x \mapsto e^{-itx}$ is the pointwise complex conjugate of the function $x \mapsto e^{itx}$.

For any real numbers $t$ and $s$, there exists a constant $C$ such that for all $x \in \mathbb{R}$, the norm of the difference between the exponential multipliers is bounded: $$\| e^{itx} - e^{isx} \| \leq C$$

For any real numbers $t$ and $s$, the exponential multiplier function $x \mapsto e^{i(t+s)x}$ is equal to the pointwise product of the functions $x \mapsto e^{itx}$ and $x \mapsto e^{isx}$.

Given a spectral measure $\mu_S$ on $\mathbb{R}$ (acting on a Hilbert space $H$) and a real parameter $t \in \mathbb{R}$, this definition constructs the bounded operator obtained by integrating the function $x \mapsto e^{itx}$ with respect to $\mu_S$. In the context of Stone's theorem, this corresponds to the unitary operator $e^{itT}$ generated by the self-adjoint operator $T$ associated with the spectral measure, expressed as: $$\exp(itT) = \int_{\mathbb{R}} e^{itx} \, d\mu_S(x)$$

Let $\mu_S$ be a spectral measure on $\mathbb{R}$ acting on a Hilbert space $H$. For any real numbers $t$ and $s$, let the operator $\exp(itT)$ be defined by the spectral integral $\int_{\mathbb{R}} e^{itx} \, d\mu_S(x)$. Then the group law holds: $$\exp(i(t+s)T) = \exp(itT) \exp(isT)$$

Let $\mu_S$ be a spectral measure on $\mathbb{R}$ acting on a Hilbert space $H$. The operator $\exp(itT)$ evaluated at $t = 0$, defined as the integral of the function $x \mapsto e^{i \cdot 0 \cdot x} = 1$ with respect to $\mu_S$, is the identity operator $I$ on $H$. That is, $\exp(i \cdot 0 \cdot T) = \int_{\mathbb{R}} 1 \, d\mu_S(x) = I$.

Let $\mu_S$ be a spectral measure on $\mathbb{R}$ acting on a Hilbert space $H$. For any $t \in \mathbb{R}$, let $\exp(itT)$ be the operator defined by the spectral integral $\int_{\mathbb{R}} e^{itx} \, d\mu_S(x)$. Then the product of $\exp(-itT)$ and $\exp(itT)$ is the identity operator $I$ on $H$: $$\exp(-itT) \exp(itT) = I$$

Let $\mu_S$ be a spectral measure on $\mathbb{R}$ acting on a Hilbert space $H$. For any $t \in \mathbb{R}$, let $\exp(itT)$ denote the operator defined by the spectral integral $\int_{\mathbb{R}} e^{itx} \, d\mu_S(x)$. Then the product of $\exp(itT)$ and $\exp(-itT)$ is the identity operator $I$ on $H$: $$\exp(itT) \exp(-itT) = I$$

Let $\mu_S$ be a spectral measure on $\mathbb{R}$ acting on a Hilbert space $H$. For any real parameter $t \in \mathbb{R}$, let $\exp(itT) = \int_{\mathbb{R}} e^{itx} \, d\mu_S(x)$ be the operator defined by the integral of the exponential multiplier. Then the adjoint of this operator satisfies: $$(\exp(itT))^* = \exp(-itT)$$ where $\exp(-itT) = \int_{\mathbb{R}} e^{-itx} \, d\mu_S(x)$.

Let $\mu_S$ be a spectral measure on $\mathbb{R}$ acting on a Hilbert space $H$, and let $t \in \mathbb{R}$. Then the operator defined by the spectral integral $$e^{itT} = \int_{\mathbb{R}} e^{itx} \, d\mu_S(x)$$ is a unitary operator on $H$.

Let $H$ be a nonempty Hilbert space and $\mu_S$ be a spectral measure on $\mathbb{R}$ (acting on $H$). For any real numbers $t, s \in \mathbb{R}$ and any vector $x \in H$, the difference between the actions of the unitary operators $e^{itT}$ and $e^{isT}$ on $x$ is equal to the integral of the difference of their corresponding multipliers: $$\exp(itT)x - \exp(isT)x = \left( \int_{\mathbb{R}} (e^{itz} - e^{isz}) \, d\mu_S(z) \right) x$$ where $\exp(itT)$ is the unitary operator defined by the spectral integral $\int_{\mathbb{R}} e^{itz} \, d\mu_S(z)$.

Let $H$ be a Hilbert space and $\mu_S$ be a spectral measure on $\mathbb{R}$ taking values in the bounded operators on $H$. For any vector $x \in H$, the map $t \mapsto \left( \int_{\mathbb{R}} e^{it\lambda} \, d\mu_S(\lambda) \right) x$ is continuous from $\mathbb{R}$ to $H$. This integral defines the unitary operator $e^{itT}$ where $T$ is the self-adjoint operator associated with $\mu_S$.

This instance allows a strongly continuous one-parameter unitary group $G$ on a Hilbert space $H$ to be treated as a function. It maps each real number $t \in \mathbb{R}$ to a continuous linear operator $G(t) \in \mathcal{L}(H)$.

For any strongly continuous one-parameter unitary group $G$ acting on a Hilbert space $H$, the value of the group at the parameter $t = 0$ is the identity operator, i.e., $G(0) = I$.

Let $H$ be a Hilbert space and $G$ be a strongly continuous unitary one-parameter group on $H$. For any real numbers $t$ and $s$, the group property holds such that the operator at $t + s$ is the composition of the operators at $t$ and $s$: $G(t + s) = G(t) G(s)$.

Let $H$ be a Hilbert space and let $G$ be a strongly continuous one-parameter unitary group on $H$. For any real number $t$, the operator $G(t)$ is a unitary operator.

Let $H$ be a Hilbert space and let $G$ be a strongly continuous one-parameter unitary group on $H$. For any vector $x \in H$, the mapping $t \mapsto G(t)x$ from $\mathbb{R}$ to $H$ is continuous.

Given a spectral measure $\mu_S$ on $\mathbb{R}$ acting on a Hilbert space $H$, this definition constructs the strongly continuous one-parameter unitary group $U: \mathbb{R} \to \mathcal{B}(H)$. For each real number $t$, the operator $U(t)$ is defined by the spectral integral: $$U(t) = \int_{\mathbb{R}} e^{itx} \, d\mu_S(x)$$ This collection of operators forms a group under composition such that $U(0) = I$ and $U(t+s) = U(t)U(s)$, where each $U(t)$ is a unitary operator and the map $t \mapsto U(t)x$ is continuous for every vector $x \in H$.