Physlib

Physlib.ProbabilisticTheory.Effect.Basic

Effects

i. Overview

An effect models a yes/no measurement outcome, ranging continuously between the impossible outcome `0` and the certain outcome `1`. Formally, it is a point of the order interval `[0, 1]` inside `E`. For self-adjoint matrices, effects are exactly the operators `0 ≤ M ≤ 1` — the elements of a POVM.

ii. Key results

- `Effect` : a bounded measurement outcome, the order interval `[0, 1]`. - `Effect.mem_iff_mem_posCone_and_one_sub_mem_posCone` : an effect is exactly a positive element whose complement from the order unit is also positive. - `Effect.exists_pos_smul_mem` : every positive observable becomes an effect after scaling it down enough.

iii. Table of contents

  • A. Effects

iv. References

- G. Ludwig, *Foundations of Quantum Mechanics I*, Springer, 1983. <https://link.springer.com/book/10.1007/978-3-642-86751-4>

A. Effects

5 declarations

theorem

A∈[0,1]  ⟺  A≥0 and 1−A≥0A \in [0, 1] \iff A \ge 0 \text{ and } 1 - A \ge 0

Let EE be an ordered vector space with a unit element 11. An element A∈EA \in E is an effect (that is, A∈[0,1]A \in [0, 1]) if and only if AA is positive (A≥0A \ge 0) and its complement 1−A1 - A is also positive (1−A≥01 - A \ge 0).

instance

Zero element of the set of effects

For an order unit space EE, the zero element for the set of effects Effect E={A∈E∣0≤A≤1}\text{Effect } E = \{ A \in E \mid 0 \le A \le 1 \} is the element 0∈E0 \in E. Since 00 satisfies the condition 0≤0≤10 \le 0 \le 1 in an order unit space, it is a valid effect, representing the impossible measurement outcome.

instance

The unit element 11 is an effect

For an order unit space EE, the unit element 1∈E1 \in E (representing the certain outcome) is an element of the set of effects [0,1][0, 1]. This definition provides the unit element 11 for the type of effects.

instance

The set of effects is non-empty

Let EE be an order unit space. The set of effects in EE, defined as the order interval [0,1]={A∈E∣0≤A≤1}[0, 1] = \{ A \in E \mid 0 \le A \le 1 \}, is non-empty.

theorem

Every positive element can be scaled into the set of effects [0,1][0, 1]

Let EE be an order unit space. For any positive element B∈EB \in E (where 0≤B0 \le B), there exists a positive scalar r>0r > 0 such that the scaled element r⋅Br \cdot B is an effect, meaning it lies within the order interval [0,1][0, 1].