MATHLIBANNEX / CANONICAL DECLARATION CARD

Pure states as real extreme points

MathlibAnnex.Analysis.CStarAlgebra.IsPureState

def

Defines purity inside the normalized positive state space.

Statement

Let be a unital complex -algebra, and let be continuous and complex-linear. Purity is the following condition on .

Definition

Write Then is pure precisely when and, whenever and satisfy one has . Equivalently, . Membership in the extreme-point set already includes membership in .

Assumptions

The definition does not require . Positivity uses the given star-compatible order on and the usual real nonnegative cone inside .

Conclusion

A pure state is in particular a state; extremality is taken for real convex combinations.

Main citations

Lean source signature (exact)

The complete declaration below is a separate exact source excerpt; the original header record is retained with the manuscript.

/-- A pure state is an extreme point of the ordinary state space. -/
def IsPureState (A : Type u) [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]
    (phi : A →L[ℂ] ℂ) : Prop :=
  phi ∈ (stateSpace A).extremePoints ℝ
In the source Mathematical meaning
(A : Type u) [CStarAlgebra A] The unital complex -algebra on which the functional is defined.
[PartialOrder A] [StarOrderedRing A] These typeclasses provide the usual order on a -algebra, equivalently when is positive. They are used by the state and positivity arguments.
(phi : A →L[ℂ] ℂ) The given continuous complex-linear functional .
: Prop The output is a property of that functional.
stateSpace A The set of all positive normalized continuous complex-linear functionals defined above.
(stateSpace A).extremePoints ℝ The real extreme points of that convex set: no nontrivial convex decomposition into two different states.
phi ∈ (stateSpace A).extremePoints ℝ The entire RHS says both that is a state and that every decomposition displayed above has .

Exact source and proof.

Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project

Earlier published Card and PDF

Exact content identity

Declaration: MathlibAnnex.Analysis.CStarAlgebra.IsPureState

Accepted content SHA-256: c7b331956d6f53324e6f8ef13356349aed2d2b2dde7380a1883ded6b990f8216

Accepted source guide SHA-256: 36eb8f04764a523c03bca697a1a1d103a6821992dcebf28731f0aba916ed01da

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑