PhyslibAlpha.AlgebraicFramework.HilbertSpace.Unbounded.Basic

Let $H$ be a complex Hilbert space. The space of continuous linear operators on $H$ equipped with the weak operator topology, denoted by $H \to_{WOT} H$, is torsion-free as an additive group. That is, for any operator $T \in H \to_{WOT} H$ and any positive integer $n$, if $nT = 0$, then $T = 0$.

This instance defines a coercion from a weak-operator-topology (WOT) spectral measure on a measurable space $\alpha$ to a vector measure on $\alpha$ with values in the space of continuous linear operators on a complex Hilbert space $H$ equipped with the weak operator topology (denoted $H \to_{WOT} H$).

Let $\alpha$ be a measurable space and $H$ be a complex Hilbert space. This instance defines a coercion from a weak-operator-topology (WOT) spectral measure $\mu$ (of type `WOTSpectralMeasure α H`) to a function. This allows a spectral measure $\mu$ to be applied to a set $A \subseteq \alpha$, returning a bounded linear operator $\mu(A)$ in the space of operators equipped with the weak operator topology, denoted as $H \to_{WOT} H$.

Let $\mu_S$ be a WOT-spectral measure on a set $\alpha$ taking values in the space of bounded linear operators on a complex Hilbert space $\mathcal{H}$ equipped with the weak operator topology. For any subset $A \subseteq \alpha$, the operator $\mu_S(A)$ is a star projection (that is, it is both self-adjoint and idempotent).

Let $\mu$ be a weak-operator-topology spectral measure (a `WOTSpectralMeasure`) on a measurable space $\alpha$ with values in the bounded operators on a Hilbert space $H$. The measure of the universal set $\alpha$ is equal to the identity operator $I$ on $H$, denoted as $\mu(\alpha) = 1$.

Let $\alpha$ be a measurable space and $\mu_S$ be a weak-operator-topology spectral measure on $\alpha$. If a subset $A \subseteq \alpha$ is not a measurable set, then the value of the spectral measure at $A$ is the zero operator, denoted by $\mu_S(A) = 0$.

Let $\mu_S$ be a weak-operator-topology spectral measure on a measurable space $\alpha$. For any subset $A \subseteq \alpha$, the operator $\mu_S(A)$ is idempotent, meaning that the composition of the operator with itself satisfies $\mu_S(A) \mu_S(A) = \mu_S(A)$.

Let $\mu_S$ be a weak-operator-topology (WOT) spectral measure on a measurable space $\alpha$. For any measurable sets $A, B \subseteq \alpha$, if $A$ and $B$ are disjoint (i.e., $A \cap B = \emptyset$), then the product of the corresponding operators is zero: $\mu_S(A) \mu_S(B) = 0$.

Let $H$ be a Hilbert space and $\mu$ be a spectral measure on a measurable space $\alpha$ that takes values in star-projections on $H$ and is $\sigma$-additive in the weak operator topology. For any two measurable sets $A, B \subseteq \alpha$, the product (composition) of the operators $\mu(A)$ and $\mu(B)$ satisfies $\mu(A) \mu(B) = \mu(A \cap B)$.

Let $\mu$ be a weak-operator-topology (WOT) spectral measure on a measurable space $\alpha$. For any two sets $A, B \subseteq \alpha$, the associated spectral projections $\mu(A)$ and $\mu(B)$ commute, satisfying $\mu(A)\mu(B) = \mu(B)\mu(A)$.

Given a weak-operator-topology (WOT) spectral measure $\mu$ on a measurable space $\alpha$ taking values in the bounded operators on a Hilbert space $H$, and a measurable function $f : \alpha \to \beta$ to another measurable space $\beta$, the pushforward measure $f_* \mu$ is the WOT spectral measure on $\beta$ defined by $(f_* \mu)(S) = \mu(f^{-1}(S))$ for any measurable set $S \subseteq \beta$.

Let $\mu$ be a weak-operator-topology (WOT) spectral measure on a measurable space $\alpha$. For any measurable function $f : \alpha \to \beta$ and any measurable set $S \subseteq \beta$, the pushforward measure $f_* \mu$ evaluated at $S$ is given by $$(f_* \mu)(S) = \mu(f^{-1}(S)).$$

Let $H$ be a Hilbert space and $\mu$ be a weak-operator-topology (WOT) spectral measure on a measurable space $\alpha$ taking values in the bounded operators on $H$. Given measurable functions $f: \alpha \to \beta$ and $g: \beta \to \gamma$ between measurable spaces, for any measurable set $S \subseteq \gamma$, the value of the iterated pushforward measure $g_*(f_* \mu)$ at $S$ is given by $$(g_* (f_* \mu))(S) = \mu((g \circ f)^{-1}(S))$$ where $g \circ f$ denotes the composition of the functions and $(g \circ f)^{-1}(S)$ is the preimage of $S$.

Let $\alpha, \beta$, and $\gamma$ be measurable spaces, and let $H$ be a complex Hilbert space. Suppose $\mu$ is a weak-operator-topology (WOT) spectral measure on $\alpha$ taking values in the bounded operators on $H$. For any measurable functions $f: \alpha \to \beta$ and $g: \beta \to \gamma$, the pushforward of the spectral measure $\mu$ along $f$ followed by the pushforward along $g$ is equal to the pushforward of $\mu$ along the composition $g \circ f$: $$g_* (f_* \mu) = (g \circ f)_* \mu$$

Let $\mu$ be a weak-operator-topology (WOT) spectral measure on a measurable space $\alpha$. The pushforward of $\mu$ along the identity map $\text{id} : \alpha \to \alpha$ is equal to the original measure, that is, $\text{id}_* \mu = \mu$.

Let $\alpha$ be a measurable space and $H$ a complex Hilbert space. Let $\mu S$ be a weak-operator-topology spectral measure ($WOTSpectralMeasure$) on $\alpha$ taking values in the bounded operators on $H$. For any sequence of pairwise disjoint measurable sets $f: \mathbb{N} \to \text{Set } \alpha$ and any vectors $x, y \in H$, the sum of the inner products $\langle y, \mu S(f_i) x \rangle$ converges to the inner product of the measure of the union of the sets, i.e., $$\sum_{i=0}^{\infty} \langle y, \mu S(f_i) x \rangle = \left\langle y, \mu S\left(\bigcup_{i=0}^{\infty} f_i\right) x \right\rangle$$ where the convergence is in the sense of summable families in $\mathbb{C}$.

The additive group homomorphism from the space of continuous linear operators on a complex Hilbert space $H$, denoted $\mathcal{B}(H)$, to the space of continuous linear operators on $H$ endowed with the weak operator topology, denoted $\mathcal{B}(H)_{\text{WOT}}$. This map is the identity on the underlying operators, effectively "forgetting" the norm topology in favor of the weak operator topology while preserving the additive structure.

Let $H$ be a complex Hilbert space. Let $\mathcal{B}(H)$ denote the space of bounded linear operators on $H$ equipped with the operator norm topology, and let $\mathcal{B}(H)_{\text{WOT}}$ be the same space equipped with the weak operator topology. The additive homomorphism $\text{toWOTMap} : \mathcal{B}(H) \to \mathcal{B}(H)_{\text{WOT}}$, which maps an operator in the norm topology to itself in the weak operator topology, is continuous.

Let $\alpha$ be a measurable space and $H$ be a complex Hilbert space. Given a spectral measure $\mu_S$ on $\alpha$ with values in the space of bounded linear operators $\mathcal{B}(H)$ (which is $\sigma$-additive with respect to the operator norm topology), `SpectralMeasure.toWOT` constructs the corresponding weak-operator-topology spectral measure. This measure takes the same star-projection values $\mu_S(A)$ for each measurable set $A \subseteq \alpha$, but is viewed as being $\sigma$-additive with respect to the weak operator topology on $\mathcal{B}(H)$.

Let $\alpha$ be a measurable space and $H$ be a complex Hilbert space. Let $\mu_S$ be a spectral measure on $\alpha$ taking values in the space of bounded linear operators $\mathcal{B}(H)$ (norm-topology). For any set $A \subseteq \alpha$, the value of the corresponding weak-operator-topology spectral measure $\mu_S.\text{toWOT}$ evaluated at $A$ is equal to the operator $\mu_S(A)$ viewed as an element of $\mathcal{B}(H)$ equipped with the weak operator topology.