Physicslib4.GNS.PureStateExists

Weak-* compactness of the state space

The state space of a unital C*-algebra, viewed inside the weak-* dual WeakDual ℂ A, is weak- compact* (Banach-Alaoglu): it is a weak-* closed subset of the unit ball, being the intersection of the (weak-* closed) positivity conditions 0 ≤ φ (star a * a) and the normalization φ 1 = 1. This is the first step toward the existence of pure states via Krein-Milman.

Main results

• Physicslib4.GNS.weakStateSet — the state space realized in WeakDual ℂ A.
• Physicslib4.GNS.isClosed_weakStateSet — it is weak-* closed.
• Physicslib4.GNS.isCompact_weakStateSet — it is weak-* compact.

Supporting lemmas

• State.toWeakDual_mem_weakStateSet — a state's image under State.toWeakDual lies in weakStateSet; the compatibility lemma a future Krein-Milman argument will need.

Note on pure-state existence

Concluding the existence of a pure state by Krein-Milman needs LocallyConvexSpace ℝ (WeakDual ℂ A), which Mathlib does not synthesize. The extreme-point-to-state transfer also needs weak-* coercion-algebra lemmas ((t • φ + (1-t) • ψ) a = t • φ a + (1-t) • ψ a) which Mathlib does not provide for WeakDual. The compactness result below is the reusable substance.

def Physicslib4.GNS.weakStateSet {A : Type u_1} [CStarAlgebra A] : Set (WeakDual ℂ A)

The state space in the weak-* topology: the positive functionals φ on A with φ(1) = 1.

In the weak-* topology, functionals converge when their values φ(a) converge for every a: a sequence of states converges when all expectation values do. For a positive functional φ(1) = 1 is the same as ‖φ‖ = 1, so mathematically these are exactly the states; the library proves that every state lies in the set (State.toWeakDual, State.toWeakDual_mem_weakStateSet), not the converse. By the Banach–Alaoglu theorem the set is weak-* compact (isCompact_weakStateSet), which with the Krein–Milman theorem gives the existence of pure states; the library proves the compactness, not the existence.

Implementation note: the set lives in Mathlib's WeakDual ℂ A, whose topology is the weak-* topology; stateSpace is the same set of functionals with the norm topology.

Blueprint: thrm:state-space-weak-compact

Equations

• Physicslib4.GNS.weakStateSet = {φ : WeakDual ℂ A | (∀ (a : A), 0 ≤ φ (star a * a)) ∧ φ 1 = 1}

noncomputable def Physicslib4.GNS.State.toWeakDual {A : Type u_1} [CStarAlgebra A] (ω : State A) : WeakDual ℂ A

A state, viewed as an element of the weak-* dual.

Equations

• ω.toWeakDual = StrongDual.toWeakDual ω.toContinuousLinearMap

@[simp]

theorem Physicslib4.GNS.State.toWeakDual_apply {A : Type u_1} [CStarAlgebra A] (ω : State A) (a : A) : ω.toWeakDual a = ω a

theorem Physicslib4.GNS.State.toWeakDual_mem_weakStateSet {A : Type u_1} [CStarAlgebra A] (ω : State A) : ω.toWeakDual ∈ weakStateSet

theorem Physicslib4.GNS.isClosed_complex_nonneg : IsClosed {z : ℂ | 0 ≤ z}

The nonnegative reals inside ℂ form a closed set.

theorem Physicslib4.GNS.isClosed_weakStateSet {A : Type u_1} [CStarAlgebra A] : IsClosed weakStateSet

The state set is weak-* closed.

theorem Physicslib4.GNS.isCompact_weakStateSet {A : Type u_1} [CStarAlgebra A] : IsCompact weakStateSet

Banach–Alaoglu for states. The state set is weak-* compact.