Physlib

PhyslibAlpha.ProbabilisticTheory.State.Pairing

The state–effect pairing

i. Overview

States and effects are paired by evaluation, `(ω, e) ↦ ω e ∈ [0, 1]`. This pairing is affine in both arguments. It also separates both spaces: a state is determined by its values on all effects, and an effect is determined by its values under all states. Moreover, the distance between two effects is the largest difference in probability that they can produce over all states.

Thus states and effects admit faithful representations as probability-valued functions on one another.

ii. Key results

  • `UnitalPositiveLinearMap.apply_mem_Icc` : state–effect evaluation takes values in `[0, 1]`.
  • `UnitalPositiveLinearMap.apply_mix` : evaluation is affine in the effect argument.
  • `UnitalPositiveLinearMap.ext_of_effect_eq` : effects separate states.
  • `Effect.dist_eq_sSup_abs_apply` : effect distance is determined by state evaluations.
  • `Effect.ext_of_forall_apply_eq` : states separate effects.
  • `UnitalPositiveLinearMap.injective_apply_effect` : states embed into functions on effects.
  • `Effect.injective_apply_state` : effects embed into functions on states.

iii. Table of contents

  • A. State–effect evaluation
  • B. Effects separate states
  • C. States separate effects

A. State–effect evaluation

B. Effects separate states

C. States separate effects

8 declarations

theorem

ω(e)∈[0,1]\omega(e) \in [0, 1] for state ω\omega and effect ee

Let EE be a type equipped with an additive commutative group structure, a partial order, and a unit element 11. For any state ω\omega (defined as a unital positive linear map from EE to R\mathbb{R}) and any effect e∈Ee \in E (where 0≤e≤10 \le e \le 1), the evaluation ω(e)\omega(e) lies in the unit interval [0,1][0, 1].

theorem

State Evaluation is Affine on Effects: ω(te+(1−t)f)=tω(e)+(1−t)ω(f)\omega(t e + (1 - t) f) = t \omega(e) + (1 - t) \omega(f)

Let EE be a partially ordered additive commutative group with a unit element 11. Let ω∈S[R,E]\omega \in \mathcal{S}[\mathbb{R}, E] be a state, represented as a unital positive linear map from EE to R\mathbb{R}. For any two effects e,f∈[0,1]⊆Ee, f \in [0, 1] \subseteq E and any scalar tt in the unit interval [0,1]⊆R[0, 1] \subseteq \mathbb{R}, the evaluation of the state ω\omega on the probabilistic mixture of effects is affine: ω(te+(1−t)f)=tω(e)+(1−t)ω(f)\omega(t e + (1 - t) f) = t \omega(e) + (1 - t) \omega(f)

theorem

States agreeing on effects agree on non-negative elements

Let EE be an ordered additive commutative group with a unit 11. Let ω\omega and ϕ\phi be states (unital positive linear maps) from EE to R\mathbb{R}. If ω(e)=ϕ(e)\omega(e) = \phi(e) for every effect e∈Ee \in E (where an effect is an element satisfying 0≤e≤10 \le e \le 1), then for any non-negative element B∈EB \in E (satisfying B≥0B \ge 0), it holds that ω(B)=ϕ(B)\omega(B) = \phi(B).

theorem

Effects separate states

Let EE be an ordered additive commutative group with a unit element 11. Let ω\omega and ϕ\phi be unital positive linear maps from EE to R\mathbb{R} (representing states). If ω(e)=ϕ(e)\omega(e) = \phi(e) for every effect e∈Ee \in E (where an effect is any element ee such that 0≤e≤10 \le e \le 1), then the states are equal, i.e., ω=ϕ\omega = \phi.

theorem

The state-effect evaluation map ω↦ω∣Effect E\omega \mapsto \omega|_{\text{Effect } E} is injective.

Let EE be an ordered additive commutative group with a unit element 11. Let S[R,E]\mathcal{S}[\mathbb{R}, E] denote the set of states, which are unital positive linear maps from EE to R\mathbb{R}. Let Effect E\text{Effect } E be the set of elements e∈Ee \in E such that 0≤e≤10 \le e \le 1. The mapping that assigns to each state ω∈S[R,E]\omega \in \mathcal{S}[\mathbb{R}, E] the function e↦ω(e)e \mapsto \omega(e) defined on the set of effects is injective. In other words, a state is uniquely determined by its values on all effects.

theorem

d(e,f)=sup⁡ω∣ω(e)−ω(f)∣d(e, f) = \sup_{\omega} |\omega(e) - \omega(f)| for effects e,fe, f and states ω\omega

Let EE be a nontrivial ordered additive commutative group with a unit element 11. For any two effects ee and ff in EE (elements such that 0≤e,f≤10 \le e, f \le 1), the distance between them is equal to the supremum of the absolute difference of their evaluations over all states ω∈S[R,E]\omega \in \mathcal{S}[\mathbb{R}, E], where states are defined as unital positive linear maps from EE to R\mathbb{R}. Mathematically, d(e,f)=sup⁡ω∈S[R,E]∣ω(e)−ω(f)∣.d(e, f) = \sup_{\omega \in \mathcal{S}[\mathbb{R}, E]} |\omega(e) - \omega(f)|.

theorem

States separate effects

Let EE be a partially ordered additive commutative group with a unit element 11. We define an **effect** as an element e∈Ee \in E such that 0≤e≤10 \le e \le 1. Let S(R,E)\mathcal{S}(\mathbb{R}, E) denote the space of states, which are unital positive linear maps from EE to R\mathbb{R}. For any two effects e,f∈Ee, f \in E, if ω(e)=ω(f)\omega(e) = \omega(f) for every state ω∈S(R,E)\omega \in \mathcal{S}(\mathbb{R}, E), then e=fe = f.

theorem

States Separate Effects

Let EE be an ordered additive commutative group with a unit element 11. Let Effect(E)\text{Effect}(E) be the set of elements e∈Ee \in E such that 0≤e≤10 \le e \le 1, and let S(E)\mathcal{S}(E) be the space of states (unital positive linear maps from EE to R\mathbb{R}). Then the evaluation map that sends an effect e∈Effect(E)e \in \text{Effect}(E) to the function ω↦ω(e)\omega \mapsto \omega(e) on the state space S(E)\mathcal{S}(E) is injective.