5. Positive Linear Functionals and States
Let M be a W^*-algebra and let T denote the set of all \sigma-continuous positive
linear functionals on M, and E the linear space of all finite linear combinations of
elements of T. Let P and M^s denote the set of positive elements and the set of
self-adjoint elements of M, respectively.
P is a convex cone in M.
Lean code for Lemma5.1●1 definition
Associated Lean declarations
-
ConvexCone.positive[complete]
-
ConvexCone.positive[complete]
-
defdefined in Mathlib/Geometry/Convex/Cone/Basic.leancomplete
def ConvexCone.positive.{u_2, u_4} (R : Type u_2) (M : Type u_4) [Semiring R] [PartialOrder R] [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] [Module R M] [PosSMulMono R M] : ConvexCone R M
def ConvexCone.positive.{u_2, u_4} (R : Type u_2) (M : Type u_4) [Semiring R] [PartialOrder R] [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] [Module R M] [PosSMulMono R M] : ConvexCone R M
The positive cone is the convex cone formed by the set of nonnegative elements in an ordered module.
-
Ultraweak.isClosed_setOf_isSelfAdjoint[complete] -
Ultraweak.isClosed_nonneg[complete]
(Sakai 1.7.1) P and M^s are \sigma-closed.
Lean code for Lemma5.2●2 theorems
Associated Lean declarations
-
Ultraweak.isClosed_setOf_isSelfAdjoint[complete]
-
Ultraweak.isClosed_nonneg[complete]
-
Ultraweak.isClosed_setOf_isSelfAdjoint[complete] -
Ultraweak.isClosed_nonneg[complete]
-
theoremdefined in LeanOA/Ultraweak/OrderClosed.leancomplete
theorem Ultraweak.isClosed_setOf_isSelfAdjoint.{u_1, u_2} {M : Type u_1} {P : Type u_2} [CStarAlgebra M] [NormedAddCommGroup P] [NormedSpace ℂ P] [Predual ℂ M P] [CompleteSpace P] : IsClosed {x | IsSelfAdjoint x}
theorem Ultraweak.isClosed_setOf_isSelfAdjoint.{u_1, u_2} {M : Type u_1} {P : Type u_2} [CStarAlgebra M] [NormedAddCommGroup P] [NormedSpace ℂ P] [Predual ℂ M P] [CompleteSpace P] : IsClosed {x | IsSelfAdjoint x}
The selfadjoint elements are closed in the ultraweak topology.
-
theoremdefined in LeanOA/Ultraweak/OrderClosed.leancomplete
theorem Ultraweak.isClosed_nonneg.{u_1, u_2} {M : Type u_1} {P : Type u_2} [CStarAlgebra M] [NormedAddCommGroup P] [NormedSpace ℂ P] [Predual ℂ M P] [CompleteSpace P] [PartialOrder M] [StarOrderedRing M] : IsClosed {x | 0 ≤ x}
theorem Ultraweak.isClosed_nonneg.{u_1, u_2} {M : Type u_1} {P : Type u_2} [CStarAlgebra M] [NormedAddCommGroup P] [NormedSpace ℂ P] [Predual ℂ M P] [CompleteSpace P] [PartialOrder M] [StarOrderedRing M] : IsClosed {x | 0 ≤ x}
The nonnegative elements are closed in the ultraweak topology.
(Sakai 1.7.2) For any self-adjoint element a \notin P, there exists \varphi \in T such
that \varphi(a) < 0.
Lean code for Lemma5.3●1 theorem
Associated Lean declarations
-
theoremdefined in LeanOA/Ultraweak/SeparatingDual.leancomplete
theorem Ultraweak.exists_positiveCLM_apply_lt_zero.{u_1, u_2} {M : Type u_1} {P : Type u_2} [CStarAlgebra M] [PartialOrder M] [StarOrderedRing M] [NormedAddCommGroup P] [NormedSpace ℂ P] [Predual ℂ M P] [CompleteSpace P] (a : Ultraweak ℂ M P) (ha₁ : IsSelfAdjoint a) (ha₂ : ¬0 ≤ a) : ∃ φ, φ a < 0
theorem Ultraweak.exists_positiveCLM_apply_lt_zero.{u_1, u_2} {M : Type u_1} {P : Type u_2} [CStarAlgebra M] [PartialOrder M] [StarOrderedRing M] [NormedAddCommGroup P] [NormedSpace ℂ P] [Predual ℂ M P] [CompleteSpace P] (a : Ultraweak ℂ M P) (ha₁ : IsSelfAdjoint a) (ha₂ : ¬0 ≤ a) : ∃ φ, φ a < 0
If `a : σ(M, P)` is a selfadjoint element which is not nonnegative, then there is some positive continuous linear functional which takes a negative value at `a`. This is Sakai 1.7.2. Our approach is essentially the same, but instead of applying Hahn-Banach to the `ℝ`-locally convex space of selfadjoint elements and then extending this functional to `ℂ`-linear one defined everywhere, we apply it for `σ(M, P)` and then precompose with the real part before extending to a `ℂ`-linear functional.
By Lemma 5.1 and Lemma 5.2, P is a
\sigma-closed convex cone in the real locally convex space M^s. By the Hahn-Banach
Separation Theorem, there is a \sigma-continuous real linear functional g on M^s
such that \inf_{h \in P} g(h) > g(a). Since P is a cone, if g(h) < 0 then we could
scale h by a positive constant so that g(ch) \le g(a), which is nonsense. Therefore
g(h) \ge 0 for all h \ge 0, and the infimum above must be zero (which can again be seen
by scaling). It follows that 0 > g(a).
To appropriately extend g to a functional on M, define
\varphi(a + ib) = g(a) + i g(b) for any a, b \in M^s. This \varphi is a (complex)
linear functional on M, and the *-operation is \sigma-continuous because M^s is
\sigma-closed (by Lemma 5.2). It follows that
\varphi is a \sigma-continuous positive linear functional on M such that
\varphi(a) = g(a) < 0.
If a \in M, and \psi(a) = 0 for every \psi \in T, then a = 0.
Lean code for Lemma5.4●1 theorem
Associated Lean declarations
-
Ultraweak.ext_positiveCLM[complete]
-
Ultraweak.ext_positiveCLM[complete]
-
theoremdefined in LeanOA/Ultraweak/SeparatingDual.leancomplete
theorem Ultraweak.ext_positiveCLM.{u_1, u_2} {M : Type u_1} {P : Type u_2} [CStarAlgebra M] [PartialOrder M] [StarOrderedRing M] [NormedAddCommGroup P] [NormedSpace ℂ P] [Predual ℂ M P] [CompleteSpace P] {a b : Ultraweak ℂ M P} (h : ∀ (φ : Ultraweak ℂ M P →P[ℂ] ℂ), φ a = φ b) : a = b
theorem Ultraweak.ext_positiveCLM.{u_1, u_2} {M : Type u_1} {P : Type u_2} [CStarAlgebra M] [PartialOrder M] [StarOrderedRing M] [NormedAddCommGroup P] [NormedSpace ℂ P] [Predual ℂ M P] [CompleteSpace P] {a b : Ultraweak ℂ M P} (h : ∀ (φ : Ultraweak ℂ M P →P[ℂ] ℂ), φ a = φ b) : a = b
Given nonzero a \in P in M, since P is a cone, -a \notin P. By
Lemma 5.3, there is a \varphi \in T such
that \varphi(-a) < 0, hence \varphi(a) > 0. The desired statement follows by
contraposition.