PhyslibAlpha.ProbabilisticTheory.Effect.Basic

For a type $E$ equipped with a partial order $\le$, a zero element $0$, and a unit element $1$, the set of **effects** is the order interval $[0, 1]$ in $E$. An element $A \in E$ is an effect if it satisfies $0 \le A \le 1$. In the context of probabilistic theories and quantum mechanics, these represent bounded measurement outcomes ranging from the impossible outcome $0$ to the certain outcome $1$.

In an additive commutative group $E$ equipped with a partial order and a unit element $1$, an element $A \in E$ is an effect (i.e., $0 \le A \le 1$) if and only if $A$ is in the positive cone $\text{PosCone}(E)$ and its complement from the unit, $1 - A$, is also in the positive cone $\text{PosCone}(E)$. Here, $\text{PosCone}(E)$ is defined as the set of elements $x \in E$ such that $0 \le x$.

For a type $E$ equipped with an additive commutative group structure, a partial order, and a unit element $1$, the zero element $0 \in E$ is an effect, belonging to the interval $[0, 1]$.

For an additive commutative group $E$ with a partial order and a unit element $1$, the identity element $1 \in E$ is an effect, as it satisfies the condition $0 \le 1 \le 1$. This definition identifies $1$ as the "certain outcome" within the set of effects $[0, 1]$.

Let $E$ be a partially ordered additive commutative group with a unit element $1$. The set of effects, defined as the order interval $[0, 1] = \{e \in E \mid 0 \le e \le 1\}$, is non-empty.

Let $E$ be a type equipped with a partial order $\le$, a zero element $0$, and a unit element $1$. The zero element of the set of effects (the order interval $[0, 1] \subseteq E$) is equal to the zero element $0$ of the underlying type $E$.

Let $E$ be a type equipped with a partial order, a zero element $0$, and a unit element $1$. In the set of effects $[0, 1] \subseteq E$, the unit element $1$ corresponds to the unit element $1$ of the base space $E$.

For a type $E$ equipped with an additive commutative group structure, a partial order, and a unit element $1$, two effects $e_1, e_2 \in [0, 1]$ are defined to be **orthogonal** if their sum is less than or equal to the unit element, i.e., $e_1 + e_2 \le 1$.

For an ordered additive commutative group $E$ with a unit element $1$, let $e$ and $f$ be two effects (elements in the interval $[0, 1] \subseteq E$). If $e$ and $f$ are orthogonal (typically meaning $e + f \le 1$), this function returns their sum $e + f$ as an effect in $[0, 1]$.

Let $E$ be an ordered additive commutative group with a unit element $1$. We define an **effect** as an element $e \in E$ such that $0 \le e \le 1$. For any two effects $e$ and $f$ that are orthogonal, the value of their sum as defined for effects is equal to their algebraic sum $e + f$ in the group $E$.

Let $E$ be a partially ordered additive commutative group with a unit element $1$. For any non-negative element $B \in E$ (that is, $0 \le B$), there exists a positive real number $r > 0$ such that $r \cdot B$ is an effect, meaning $0 \le r \cdot B \le 1$. In physical terms, every non-negative observable can be scaled down by a sufficiently large positive real number to become an effect.