Pure state as an extreme point

MathlibAnnex.Analysis.CStarAlgebra.IsPureState

def

Defines pure states as the real extreme points of the state space.

Statement

Let A be a unital complex C*-algebra and let φ : A → ℂ be a continuous complex-linear functional. φ is pure exactly when it belongs to the real extreme points of the normalized positive state space stateSpace A. Membership in that extreme-point set includes membership in the state space.

Definition

IsPureState A φ ↔ φ ∈ (stateSpace A).extremePoints ℝ.

Assumptions

Let A be a unital complex C*-algebra and let φ : A → ℂ be a continuous complex-linear functional.

Conclusion

φ is pure exactly when it belongs to the real extreme points of the normalized positive state space stateSpace A. Membership in that extreme-point set includes membership in the state space.

Main citations

Lean source signature (exact)

def IsPureState (A : Type u) [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]
    (phi : A →L[ℂ] ℂ) : Prop

Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Card JSON