Exact source: MathlibAnnex/Analysis/CStarAlgebra/State/Basic.lean
Pinned GitHub source · Raw UTF-8 source
Back to Pure states as real extreme points · Back to A character extends to a pure state · Back to The GNS representation of a pure state is irreducible
1import Mathlib.Analysis.Convex.Extreme2import Mathlib.Analysis.CStarAlgebra.PositiveLinearMap3import Mathlib.Analysis.Normed.Module.Normalize4import MathlibAnnex.Analysis.CStarAlgebra.CyclicTransport5import MathlibAnnex.Analysis.CStarAlgebra.GNS.Adapters6import MathlibAnnex.Analysis.CStarAlgebra.Representation.Adapters7import MathlibAnnex.Analysis.CStarAlgebra.Representation.VectorFunctional89/-!10# States and their cyclic GNS representations1112This file gives neutral mathematical names to normalized positive continuous13functionals and records the elementary bridges to Mathlib's GNS construction.14It is independent of the legacy project namespace.15-/1617set_option autoImplicit false1819open Set20open scoped ComplexOrder InnerProduct2122namespace MathlibAnnex.Analysis.CStarAlgebra2324universe u v2526variable {A : Type u} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]27variable {H : Type v}28variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]2930/-- Normalized positive continuous complex-linear functionals. -/31def 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}3435/-- A pure state is an extreme point of the ordinary state space. -/36def IsPureState (A : Type u) [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]37 (phi : A →L[ℂ] ℂ) : Prop :=38 phi ∈ (stateSpace A).extremePoints ℝ3940/-- Rebundle a state as the positive linear map used by the GNS construction. -/41def positiveLinearMapOfMemStateSpace42 (phi : A →L[ℂ] ℂ) (hphi : phi ∈ stateSpace A) : A →ₚ[ℂ] ℂ where43 toLinearMap := phi.toLinearMap44 monotone' := by45 intro a b hab46 apply sub_nonneg.mp47 change 0 ≤ phi b - phi a48 rw [← map_sub]49 exact hphi.1 (b - a) (sub_nonneg.mpr hab)5051@[simp]52theorem positiveLinearMapOfMemStateSpace_apply53 (phi : A →L[ℂ] ℂ) (hphi : phi ∈ stateSpace A) (a : A) :54 positiveLinearMapOfMemStateSpace phi hphi a = phi a :=55 rfl5657@[simp]58theorem positiveLinearMapOfMemStateSpace_one59 (phi : A →L[ℂ] ℂ) (hphi : phi ∈ stateSpace A) :60 positiveLinearMapOfMemStateSpace phi hphi 1 = 1 :=61 hphi.26263/-- The canonical vector of the GNS representation of a state. -/64noncomputable def stateGNSVector (phi : A →L[ℂ] ℂ) (hphi : phi ∈ stateSpace A) :65 (positiveLinearMapOfMemStateSpace phi hphi).GNS :=66 _root_.PositiveLinearMap.gnsCyclicVector (positiveLinearMapOfMemStateSpace phi hphi)6768theorem norm_stateGNSVector (phi : A →L[ℂ] ℂ) (hphi : phi ∈ stateSpace A) :69 ‖stateGNSVector phi hphi‖ = 1 :=70 _root_.PositiveLinearMap.norm_gnsCyclicVector _71 (positiveLinearMapOfMemStateSpace_one phi hphi)7273theorem inner_gnsStarAlgHom_stateGNSVector74 (phi : A →L[ℂ] ℂ) (hphi : phi ∈ stateSpace A) (a : A) :75 inner ℂ (stateGNSVector phi hphi)76 ((positiveLinearMapOfMemStateSpace phi hphi).gnsStarAlgHom a77 (stateGNSVector phi hphi)) = phi a := by78 exact _root_.PositiveLinearMap.inner_gnsCyclicVector_gnsStarAlgHom _ a7980theorem denseRange_gnsStarAlgHom_stateGNSVector81 (phi : A →L[ℂ] ℂ) (hphi : phi ∈ stateSpace A) :82 DenseRange (fun a : A ↦83 (positiveLinearMapOfMemStateSpace phi hphi).gnsStarAlgHom a84 (stateGNSVector phi hphi)) :=85 _root_.PositiveLinearMap.denseRange_gnsStarAlgHom_apply_gnsCyclicVector _8687/-- A unit vector in a unital star representation defines a state. -/88theorem vectorFunctional_mem_stateSpace89 (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (xi : H) (hxi : ‖xi‖ = 1) :90 Representation.vectorFunctional pi xi ∈ stateSpace A := by91 refine ⟨?_, Representation.vectorFunctional_one pi hxi⟩92 intro a ha93 exact Representation.vectorFunctional_nonnegative pi xi ha9495/-- The positive functional associated to a unit vector state. -/96noncomputable def vectorPositiveFunctional97 (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (xi : H) (hxi : ‖xi‖ = 1) : A →ₚ[ℂ] ℂ :=98 positiveLinearMapOfMemStateSpace (Representation.vectorFunctional pi xi)99 (vectorFunctional_mem_stateSpace pi xi hxi)100101@[simp]102theorem vectorPositiveFunctional_apply103 (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (xi : H) (hxi : ‖xi‖ = 1) (a : A) :104 vectorPositiveFunctional pi xi hxi a = inner ℂ xi (pi a xi) :=105 rfl106107/-- A unit cyclic representation is unitarily equivalent to the GNS model of108its vector state. -/109theorem vectorState_unitaryEquivalent_gns110 (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (xi : H) (hxi : ‖xi‖ = 1)111 (hcyclic : DenseRange (StarAlgHom.orbitMap pi xi)) :112 Representation.UnitaryEquivalent pi113 (vectorPositiveFunctional pi xi hxi).gnsStarAlgHom := by114 obtain ⟨W, hW, -⟩ := StarAlgHom.existsUnique_pointedCyclicTransport115 pi (vectorPositiveFunctional pi xi hxi).gnsStarAlgHom xi116 (_root_.PositiveLinearMap.gnsCyclicVector (vectorPositiveFunctional pi xi hxi))117 hcyclic118 (_root_.PositiveLinearMap.denseRange_gnsStarAlgHom_apply_gnsCyclicVector _)119 (fun a => by120 calc121 inner ℂ xi (pi a xi) = vectorPositiveFunctional pi xi hxi a :=122 (vectorPositiveFunctional_apply pi xi hxi a).symm123 _ = inner ℂ (_root_.PositiveLinearMap.gnsCyclicVector _)124 ((vectorPositiveFunctional pi xi hxi).gnsStarAlgHom a125 (_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)129130end MathlibAnnex.Analysis.CStarAlgebra