Physlib

PhyslibAlpha.AlgebraicFramework.StarAlgebra.Observable

Observables

An observable is a self-adjoint element of a space with an additive involution. This definition needs neither multiplication nor a norm. In particular, the self-adjoint part of a complex operator algebra is already an observable space before any C⋆-algebraic structure is used.

A complex state on a starred space restricts to a real state on its observables. Thus the expectation-value functional is itself an instance of the general state notion `𝓢[ℝ, Observable A]`; it does not require a separate definition of linearity, positivity, or normalization.

The abstract order-unit case

When `E` already is a real ordered vector space (rather than the self-adjoint part of a complex one), no restriction is needed at all: `Observable E ⊆ E` directly, and a state `s : 𝓢[ℝ, E]` is already linear and positive on all of `E`, so it pairs with an observable `a : Observable E` by simply evaluating `s (a : E)`. Linearity (`map_add`, `map_smul`), positivity of a positive observable's expectation (`map_nonneg`), and the expectation of the unit observable (`map_one`) are consequently not new facts about states meeting observables — they are the same generic `UnitalPositiveLinearMap` lemmas already used everywhere else, applied at `a : E`. The examples below witness this; no bespoke `expectation` definition is needed.

Main definitions

- `Observable A`, `PositiveObservable A` - `UnitalPositiveLinearMap.onObservables` : the real state on observables induced by a complex state on the ambient starred space.

4 declarations

abbrev

The set of observables in a starred space AA as self-adjoint elements a=a∗a = a^*

For an additive group AA equipped with an additive star-involution x↦x∗x \mapsto x^* (a map such that (x+y)∗=x∗+y∗(x+y)^* = x^* + y^* and x∗∗=xx^{**} = x), an **observable** is defined as a self-adjoint element of AA, which is an element a∈Aa \in A satisfying the condition a∗=aa^* = a.

abbrev

Positive observable a≥0a \ge 0 in AA

Let AA be an additive group equipped with an additive star-involution x↦x∗x \mapsto x^* and a partial order ≤\le. A **positive observable** is an element a∈Aa \in A that is both an observable (i.e., it is self-adjoint, a∗=aa^* = a) and satisfies the condition 0≤a0 \le a.

definition

Real state on observables induced by a complex state ω\omega

Given a complex state ω∈S[A]\omega \in \mathcal{S}[A] on a complex starred space AA, this definition constructs the corresponding real state on the space of observables, denoted by Observable A\text{Observable } A. This is achieved by restricting the unital positive complex-linear functional ω\omega to the subspace of self-adjoint elements a∈Aa \in A (where a∗=aa^* = a). Since positive linear maps send self-adjoint elements to real values, the resulting map is a unital positive real-linear functional from Observable A\text{Observable } A to R\mathbb{R}.

theorem

The value of the restricted state ωonObservables(a)\omega_{\text{onObservables}}(a) equals ω(a)\omega(a)

Let AA be a complex starred space and ω∈S[A]\omega \in \mathcal{S}[A] be a complex state. For any observable a∈Observable Aa \in \text{Observable } A (a self-adjoint element a=a∗a = a^*), the value of the induced real state ωonObservables\omega_{\text{onObservables}} evaluated at aa is equal to the value of the original state ω\omega evaluated at aa, after regarding the real result as a complex number: (ωonObservables(a))C=ω(a)( \omega_{\text{onObservables}}(a) )_{\mathbb{C}} = \omega(a) where ωonObservables:Observable A→R\omega_{\text{onObservables}} : \text{Observable } A \to \mathbb{R} is the restriction of the unital positive linear map ω\omega to the subspace of self-adjoint elements.