PhyslibAlpha.ProbabilisticTheory.State.NormalEquivalence

Normal states give normal weights

i. Overview

The weight of a normal state is normal: suprema of directed families of nonnegative observables are suprema in the whole space, where the state is normal.

ii. Key results

`UnitalPositiveLinearMap.IsNormal.toWeight_isNormal` : normal states give normal weights.

1 declaration

theorem

Normal states induce normal weights

#toWeight_isNormal

Let $E$ be a space of observables and let $s \in \mathcal{S}[\mathbb{R}, E]$ be a state on $E$ . If $s$ is a normal state, then the weight induced by $s$ , denoted by $s.\text{toWeight}$ , is also a normal weight. Here, normality refers to the property that the map preserves the suprema of directed families of nonnegative elements.