PhyslibAlpha.AlgebraicFramework.JordanOrderUnit.JBW.ProjectionResolution

Let $E$ be a Jordan order-unit space. This definition is the unital positive linear map from $E$ to its type synonym $\text{WithOrderUnitNorm}(E)$, which represents $E$ equipped with the order-unit norm. The map is the identity on the underlying algebraic and order structures, meaning it maps each element $x \in E$ to itself while preserving the positive cone ($x \ge 0 \implies x \ge 0$) and the identity element ($1 \mapsto 1$).

Let $E$ be a Jordan order-unit space. The unital positive linear map $\text{id} : E \to \text{WithOrderUnitNorm } E$, which acts as the identity on the underlying ordered set, is normal. That is, for any non-empty directed subset $D \subseteq E$, the map preserves the least upper bound: $\text{id}(\sup D) = \sup (\text{id}(D))$.

For a JBW-algebra or an order-unit space $E$, let $\text{WithOrderUnitNorm } E$ denote the same space equipped with its order-unit norm. This definition provides the unital positive linear map from $\text{WithOrderUnitNorm } E$ back to $E$ induced by the inverse of the canonical linear isomorphism between them. This map acts as the identity on the underlying elements and satisfies the properties of being positive (mapping the positive cone to itself) and unital (mapping the identity element to itself).

Let $E$ be a JBW-algebra. The unital positive linear map $\Phi: \text{WithOrderUnitNorm } E \to E$, which identifies the space $E$ equipped with its order-unit norm with the original space $E$ (acting as the identity on elements), is normal. This means that $\Phi$ preserves the suprema of directed sets: for any non-empty directed subset $D \subseteq \text{WithOrderUnitNorm } E$ with least upper bound $x$, the image $\Phi(x)$ is the least upper bound of the set $\Phi(D)$ in $E$.

This definition represents the scalar identity channel, which is a unital positive linear map from the real numbers $\mathbb{R}$ to the space $\mathbb{R}$ equipped with its explicit order-unit-norm structure (denoted as $\text{WithOrderUnitNorm } \mathbb{R}$). The map is defined as the identity on the underlying scalars, which is inherently positive and unital (sending $1 \in \mathbb{R}$ to the order unit $1$ in $\text{WithOrderUnitNorm } \mathbb{R}$).

The unital positive linear map $\phi: \mathbb{R} \to \text{WithOrderUnitNorm } \mathbb{R}$, defined as the identity map on the real numbers, is normal. That is, it preserves the suprema of all non-empty directed sets of real numbers.

Given a state $\omega$ on an order-unit space $E$, this definition constructs a unital positive linear map (a "channel") from $E$ equipped with its explicit order-unit norm, denoted as $\text{WithOrderUnitNorm } E$, to the real numbers $\mathbb{R}$ equipped with its explicit order-unit norm. The map is the composition $i_{\mathbb{R}} \circ \omega \circ i_E^{-1}$, where $i_E^{-1}: \text{WithOrderUnitNorm } E \to E$ and $i_{\mathbb{R}}: \mathbb{R} \to \text{WithOrderUnitNorm } \mathbb{R}$ are the canonical identity maps between the spaces and their order-unit-normed versions.

Let $E$ be an order-unit space and $\omega$ be a state on $E$ (a unital positive linear map from $E$ to $\mathbb{R}$). If $\omega$ is normal—that is, it preserves the suprema of all non-empty directed sets—then the induced unital positive linear map $\tilde{\omega} : \text{WithOrderUnitNorm } E \to \text{WithOrderUnitNorm } \mathbb{R}$ (which transports $\omega$ to the spaces equipped with their explicit order-unit norms) is also normal.

Let $\Omega$ be a measurable space and $E$ be a JBW-algebra. Given a measurable projection resolution $P$ on $\Omega$ taking values in $E$ and a measurable function $f: \Omega \to \mathbb{R}$ bounded by a constant $M$ (such that $|f(x)| \le M$ for all $x \in \Omega$), this definition constructs the integral of $f$ against $P$. The integral is computed by viewing $P$ as an effect-valued measure and mapping it via the identity channel into $\text{WithOrderUnitNorm } E$ (the space $E$ equipped with its explicit order-unit norm). The result is the spectral integral: $$\int_{\Omega} f(\lambda) \, dP(\lambda)$$ which belongs to the space $\text{WithOrderUnitNorm } E$. The existence of this integral is guaranteed by the fact that JBW-algebras are complete with respect to the order-unit norm.

Let $\Omega$ be a measurable space and $E$ be a JBW-algebra. Let $P$ be a measurable projection resolution on $\Omega$ taking values in $E$. For any measurable set $s \subseteq \Omega$, let $\mathbf{1}_s: \Omega \to \mathbb{R}$ be the indicator function of $s$. The bounded Borel integral of $\mathbf{1}_s$ with respect to $P$ in the space $\text{WithOrderUnitNorm } E$ is equal to the value of the projection resolution at $s$, $P(s)$, transported through the identity map $\iota : E \to \text{WithOrderUnitNorm } E$. That is, $$\int_{\Omega} \mathbf{1}_s(\lambda) \, dP(\lambda) = \iota(P(s))$$

Let $\Omega$ be a measurable space and $E$ be a Jordan order-unit space (such as a JBW-algebra). Given a measurable projection resolution $P$ on $\Omega$ with values in $E$, a normal state $\omega$ on $E$, and a measurable function $f: \Omega \to \mathbb{R}$ bounded by some $M \in \mathbb{R}$ (such that $|f(x)| \le M$ for all $x$), this definition computes the integral of $f$ with respect to the probability measure $\mu_\omega$ induced by the state $\omega$. The measure is defined as $\mu_\omega(s) = \omega(P(s))$ for any measurable set $s \subseteq \Omega$. The result is the scalar value: $$\int_{\Omega} f(\lambda) \, d(\omega \circ P)(\lambda)$$ This value is returned as an element of the type `WithOrderUnitNorm ℝ`, which represents the real numbers equipped with the explicit order-unit norm structure.

Let $\Omega$ be a measurable space and $E$ be a JBW-algebra (or a Jordan order-unit space). Given a measurable projection resolution $P$ on $\Omega$ with values in $E$, a normal state $\omega$ on $E$, and a measurable function $f: \Omega \to \mathbb{R}$ bounded by some $M \in \mathbb{R}$ (such that $|f(x)| \le M$ for all $x \in \Omega$), this definition computes the integral of $f$ with respect to the probability measure $\mu_\omega$ induced by the state $\omega$. The measure is defined as $\mu_\omega(s) = \omega(P(s))$ for any measurable set $s \subseteq \Omega$. The result is the real scalar value: $$\int_{\Omega} f(\lambda) \, d(\omega \circ P)(\lambda)$$ This value is obtained by transporting the integral from the type `WithOrderUnitNorm ℝ` back to the standard real numbers $\mathbb{R}$ via the canonical isometry.

Given a measurable projection resolution $P$ on a measurable space $\Omega$ with values in a JBW-algebra $E$, and a normal state $\omega$ on $E$, this definition constructs a probability measure $\mu$ on $\Omega$. For any measurable set $s \subseteq \Omega$, the measure is defined as the value of the state applied to the projection associated with that set, i.e., $\mu(s) = \omega(P(s))$.

Let $E$ be a JBW-algebra and $\Omega$ be a measurable space. Let $P$ be a measurable projection resolution on $\Omega$ taking values in $E$, and let $\omega$ be a normal state on $E$. For any measurable set $s \subseteq \Omega$, the probability measure $\mu$ associated with $P$ and $\omega$ satisfies: $$\mu(s) = \omega(P(s))$$ where $P(s)$ is the spectral projection in $E$ corresponding to the event $s$.