PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.Cayley.Certificate

Let $U$ be a bounded normal operator. Suppose $D$ and $E$ are two instances of bounded normal spectral data associated with $U$. If their corresponding spectral measures are identical, then $D$ and $E$ are equal.

Let $U$ be a bounded normal operator on a complex Hilbert space. Let $D$ and $E$ be two instances of bounded normal spectral data associated with $U$. If for every measurable function $f : \mathbb{C} \to \mathbb{C}$ that is bounded (i.e., there exists a constant $C \in \mathbb{R}$ such that $\|f(z)\| \leq C$ for all $z \in \mathbb{C}$), the bounded spectral integrals are equal: $$\int_{\mathbb{C}} f \, d\mu_D = \int_{\mathbb{C}} f \, d\mu_E$$ (where $\mu_D$ and $\mu_E$ are the spectral measures associated with $D$ and $E$ respectively), then $D = E$.

For any two sets of bounded unitary spectral data $D$ and $E$ associated with a bounded unitary operator $u$, if their underlying spectral measures are equal, then the spectral data $D$ and $E$ are equal.

Let $u$ be a bounded unitary operator on a complex Hilbert space. Let $D$ and $E$ be two sets of bounded unitary spectral data associated with $u$. If for every measurable and bounded function $f : \mathbb{C} \to \mathbb{C}$, the bounded spectral integrals with respect to their corresponding spectral measures are equal, i.e., $$\int_{\mathbb{C}} f \, d\mu_D = \int_{\mathbb{C}} f \, d\mu_E,$$ then $D = E$.

For a given set of bounded unitary spectral data $D$ on a Hilbert space $H$, this definition constructs the spectral measure on the real line $\mathbb{R}$ by pulling back the complex spectral measure of $D$ through the inverse Cayley map. This resulting measure is an element of `WOTSpectralMeasure ℝ H`.

Let $D$ be a set of bounded unitary spectral data on a Hilbert space $H$. Let $D.\text{realSpectralMeasure}$ be the spectral measure on the real line $\mathbb{R}$ obtained by pulling back the complex spectral measure of $D$ through the inverse Cayley map. Then, the pushforward of $D.\text{realSpectralMeasure}$ under the Cayley map is equal to the original complex spectral measure $D.\text{spectralMeasure}$.

Let $D$ be an instance of bounded unitary spectral data on a Hilbert space $H$. For any spectral measure $\mu_S$ on the real line $\mathbb{R}$ (of type `WOTSpectralMeasure ℝ H`), if the Cayley pushforward of $\mu_S$ is equal to the complex spectral measure associated with $D$ (i.e., $\text{cayleyMap}(\mu_S) = D.\text{spectralMeasure}$), then $\mu_S$ is equal to the canonical real spectral measure $D.\text{realSpectralMeasure}$ constructed from $D$.