PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.Flow.StoneInvariance

The spectral-integral group's generator domain is invariant under its own group

The `V`-side counterpart of `StoneExistence.GeneratorInvariance.stoneCandidateGenerator_translate`: for a domain-aware spectral theorem `D : DomainAwareSelfAdjointSpectralTheorem T μS`, the operator `T` commutes with the unitary group `D.expUnitaryGroup` it generates — `D.expUnitaryGroup s` preserves `T.domain` and `T` commutes with it there. Combined with the `U`-side lemma, this is exactly the missing ingredient an ODE-uniqueness argument identifying an abstract strongly continuous unitary group with the spectral-integral group of its own generator would need on both sides (see `Existence/STONE_GENERATOR_EXISTENCE_PLAN.md`, milestone M5).

The proof is the same "shift the known derivative-at-`s`" argument `expUnitaryGroup_hasDerivAt` itself already uses internally, applied once more: differentiability of `t ↦ D.expUnitaryGroup t x` at `t = s` is exactly differentiability of `t ↦ D.expUnitaryGroup t (D.expUnitaryGroup s x)` at `t = 0`, via the group law `D.expUnitaryGroup t (D.expUnitaryGroup s x) = D.expUnitaryGroup (t + s) x`.

Main definitions

`expUnitaryGroup_translate_mem` : `D.expUnitaryGroup s` preserves `T.domain`.
`expUnitaryGroup_translate` : `T` commutes with `D.expUnitaryGroup s` on `T.domain`.

3 declarations

theorem

$U(t)U(s) = U(t+s)$ for the unitary group associated with the spectral theorem

#expUnitaryGroup_translate_comm

Let $H$ be a Hilbert space and $T$ a self-adjoint operator with a domain-aware spectral theorem $D$ . Let $U(t) = \int_{\mathbb{R}} e^{it\lambda} \, d\mu_S(\lambda)$ (denoted by `D.expUnitaryGroup t`) be the strongly continuous one-parameter unitary group associated with $T$ . For any vector $x \in H$ and any real numbers $s$ and $t$ , the group law holds: $U(t)(U(s)x) = U(t+s)x$

theorem

The Unitary Group $e^{isT}$ Preserves the Domain of $T$

#expUnitaryGroup_translate_mem

Let $H$ be a Hilbert space and $T$ be a self-adjoint operator with domain $\mathcal{D}(T) \subseteq H$ . Let $U(s) = e^{isT}$ be the strongly continuous one-parameter unitary group associated with $T$ via the spectral theorem. For any $x \in \mathcal{D}(T)$ and any $s \in \mathbb{R}$ , the vector $U(s)x$ is also contained in $\mathcal{D}(T)$ . In other words, the unitary group $U(s)$ preserves the domain of its generator $T$ .

theorem

$T$ Commutes with its Unitary Group $e^{isT}$ on $\mathcal{D}(T)$

#expUnitaryGroup_translate

Let $H$ be a Hilbert space and $T$ a self-adjoint operator with domain $\mathcal{D}(T)$ . Let $U(s) = e^{isT}$ be the strongly continuous one-parameter unitary group associated with $T$ via the spectral theorem. For any $x \in \mathcal{D}(T)$ and any $s \in \mathbb{R}$ , the vector $U(s)x$ belongs to $\mathcal{D}(T)$ and the operator $T$ commutes with the unitary group $U(s)$ such that: $T(U(s)x) = U(s)(Tx)$

PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.Flow.StoneInvariance

The spectral-integral group's generator domain is invariant under its own group

Main definitions

U(t)U(s)=U(t+s)U(t)U(s) = U(t+s)U(t)U(s)=U(t+s) for the unitary group associated with the spectral theorem

The Unitary Group eisTe^{isT}eisT Preserves the Domain of TTT

TTT Commutes with its Unitary Group eisTe^{isT}eisT on D(T)\mathcal{D}(T)D(T)

$U(t)U(s) = U(t+s)$ for the unitary group associated with the spectral theorem

The Unitary Group $e^{isT}$ Preserves the Domain of $T$

$T$ Commutes with its Unitary Group $e^{isT}$ on $\mathcal{D}(T)$