MATHLIBANNEX / EXACT SOURCE v0.4.0

MathlibAnnex.Analysis.CStarAlgebra.IsPureState

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

1 import Mathlib.Analysis.Convex.Extreme
2 import Mathlib.Analysis.CStarAlgebra.PositiveLinearMap
3 import Mathlib.Analysis.Normed.Module.Normalize
4 import MathlibAnnex.Analysis.CStarAlgebra.CyclicTransport
5 import MathlibAnnex.Analysis.CStarAlgebra.GNS.Adapters
6 import MathlibAnnex.Analysis.CStarAlgebra.Representation.Adapters
7 import MathlibAnnex.Analysis.CStarAlgebra.Representation.VectorFunctional
8 
9 /-!
10 # States and their cyclic GNS representations
11 
12 This file gives neutral mathematical names to normalized positive continuous
13 functionals and records the elementary bridges to Mathlib's GNS construction.
14 It is independent of the legacy project namespace.
15 -/
16 
17 set_option autoImplicit false
18 
19 open Set
20 open scoped ComplexOrder InnerProduct
21 
22 namespace MathlibAnnex.Analysis.CStarAlgebra
23 
24 universe u v
25 
26 variable {A : Type u} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]
27 variable {H : Type v}
28 variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
29 
30 /-- Normalized positive continuous complex-linear functionals. -/
31 def stateSpace (A : Type u) [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] :
32     Set (A →L[ℂ] ℂ) :=
33   {phi | (∀ a : A, 0 ≤ a → 0 ≤ phi a) ∧ phi 1 = 1}
34 
35 /-- A pure state is an extreme point of the ordinary state space. -/
36 def IsPureState (A : Type u) [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]
37     (phi : A →L[ℂ] ℂ) : Prop :=
38   phi ∈ (stateSpace A).extremePoints ℝ
39 
40 /-- Rebundle a state as the positive linear map used by the GNS construction. -/
41 def positiveLinearMapOfMemStateSpace
42     (phi : A →L[ℂ] ℂ) (hphi : phi ∈ stateSpace A) : A →ₚ[ℂ] ℂ where
43   toLinearMap := phi.toLinearMap
44   monotone' := by
45     intro a b hab
46     apply sub_nonneg.mp
47     change 0 ≤ phi b - phi a
48     rw [← map_sub]
49     exact hphi.1 (b - a) (sub_nonneg.mpr hab)
50 
51 @[simp]
52 theorem positiveLinearMapOfMemStateSpace_apply
53     (phi : A →L[ℂ] ℂ) (hphi : phi ∈ stateSpace A) (a : A) :
54     positiveLinearMapOfMemStateSpace phi hphi a = phi a :=
55   rfl
56 
57 @[simp]
58 theorem positiveLinearMapOfMemStateSpace_one
59     (phi : A →L[ℂ] ℂ) (hphi : phi ∈ stateSpace A) :
60     positiveLinearMapOfMemStateSpace phi hphi 1 = 1 :=
61   hphi.2
62 
63 /-- The canonical vector of the GNS representation of a state. -/
64 noncomputable def stateGNSVector (phi : A →L[ℂ] ℂ) (hphi : phi ∈ stateSpace A) :
65     (positiveLinearMapOfMemStateSpace phi hphi).GNS :=
66   _root_.PositiveLinearMap.gnsCyclicVector (positiveLinearMapOfMemStateSpace phi hphi)
67 
68 theorem norm_stateGNSVector (phi : A →L[ℂ] ℂ) (hphi : phi ∈ stateSpace A) :
69     ‖stateGNSVector phi hphi‖ = 1 :=
70   _root_.PositiveLinearMap.norm_gnsCyclicVector _
71     (positiveLinearMapOfMemStateSpace_one phi hphi)
72 
73 theorem inner_gnsStarAlgHom_stateGNSVector
74     (phi : A →L[ℂ] ℂ) (hphi : phi ∈ stateSpace A) (a : A) :
75     inner ℂ (stateGNSVector phi hphi)
76       ((positiveLinearMapOfMemStateSpace phi hphi).gnsStarAlgHom a
77         (stateGNSVector phi hphi)) = phi a := by
78   exact _root_.PositiveLinearMap.inner_gnsCyclicVector_gnsStarAlgHom _ a
79 
80 theorem denseRange_gnsStarAlgHom_stateGNSVector
81     (phi : A →L[ℂ] ℂ) (hphi : phi ∈ stateSpace A) :
82     DenseRange (fun a : A ↦
83       (positiveLinearMapOfMemStateSpace phi hphi).gnsStarAlgHom a
84         (stateGNSVector phi hphi)) :=
85   _root_.PositiveLinearMap.denseRange_gnsStarAlgHom_apply_gnsCyclicVector _
86 
87 /-- A unit vector in a unital star representation defines a state. -/
88 theorem vectorFunctional_mem_stateSpace
89     (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (xi : H) (hxi : ‖xi‖ = 1) :
90     Representation.vectorFunctional pi xi ∈ stateSpace A := by
91   refine ⟨?_, Representation.vectorFunctional_one pi hxi⟩
92   intro a ha
93   exact Representation.vectorFunctional_nonnegative pi xi ha
94 
95 /-- The positive functional associated to a unit vector state. -/
96 noncomputable def vectorPositiveFunctional
97     (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (xi : H) (hxi : ‖xi‖ = 1) : A →ₚ[ℂ] ℂ :=
98   positiveLinearMapOfMemStateSpace (Representation.vectorFunctional pi xi)
99     (vectorFunctional_mem_stateSpace pi xi hxi)
100 
101 @[simp]
102 theorem vectorPositiveFunctional_apply
103     (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (xi : H) (hxi : ‖xi‖ = 1) (a : A) :
104     vectorPositiveFunctional pi xi hxi a = inner ℂ xi (pi a xi) :=
105   rfl
106 
107 /-- A unit cyclic representation is unitarily equivalent to the GNS model of
108 its vector state. -/
109 theorem vectorState_unitaryEquivalent_gns
110     (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (xi : H) (hxi : ‖xi‖ = 1)
111     (hcyclic : DenseRange (StarAlgHom.orbitMap pi xi)) :
112     Representation.UnitaryEquivalent pi
113       (vectorPositiveFunctional pi xi hxi).gnsStarAlgHom := by
114   obtain ⟨W, hW, -⟩ := StarAlgHom.existsUnique_pointedCyclicTransport
115     pi (vectorPositiveFunctional pi xi hxi).gnsStarAlgHom xi
116     (_root_.PositiveLinearMap.gnsCyclicVector (vectorPositiveFunctional pi xi hxi))
117     hcyclic
118     (_root_.PositiveLinearMap.denseRange_gnsStarAlgHom_apply_gnsCyclicVector _)
119     (fun a => by
120       calc
121         inner ℂ xi (pi a xi) = vectorPositiveFunctional pi xi hxi a :=
122           (vectorPositiveFunctional_apply pi xi hxi a).symm
123         _ = inner ℂ (_root_.PositiveLinearMap.gnsCyclicVector _)
124             ((vectorPositiveFunctional pi xi hxi).gnsStarAlgHom a
125               (_root_.PositiveLinearMap.gnsCyclicVector _)) :=
126           (_root_.PositiveLinearMap.inner_gnsCyclicVector_gnsStarAlgHom _ a).symm)
127   refine ⟨W, fun a x ↦ ?_⟩
128   simpa using congrArg (fun T ↦ T x) (hW.2.2 a)
129 
130 end MathlibAnnex.Analysis.CStarAlgebra