Exact source: MathlibAnnex/Analysis/CStarAlgebra/PureStateGNS/State.lean
Pinned GitHub source · Raw UTF-8 source
Back to Pure CAR states admit two-sided inner intertwining sequences
1import MathlibAnnex.Analysis.CStarAlgebra.GNS.Adapters2import MathlibAnnex.Analysis.CStarAlgebra.PureStateHomogeneity.KishimotoOzawaSakai34/-! Canonical GNS data supplied by an ordinary normalized positive state. -/56set_option autoImplicit false78open Set910namespace MathlibAnnex.CStarAlgebra1112universe u1314variable {A : Type u} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]1516/-- The canonical vector of the GNS representation associated to a member of17`stateSpace`. -/18noncomputable def stateGNSVector (phi : A →L[ℂ] ℂ) (hphi : phi ∈ stateSpace A) :19 (positiveLinearMapOfMemStateSpace phi hphi).GNS :=20 _root_.PositiveLinearMap.gnsCyclicVector (positiveLinearMapOfMemStateSpace phi hphi)2122theorem norm_stateGNSVector (phi : A →L[ℂ] ℂ) (hphi : phi ∈ stateSpace A) :23 ‖stateGNSVector phi hphi‖ = 1 :=24 _root_.PositiveLinearMap.norm_gnsCyclicVector _25 (positiveLinearMapOfMemStateSpace_one phi hphi)2627/-- The original state is the vector functional of its canonical GNS vector. -/28theorem inner_gnsStarAlgHom_stateGNSVector29 (phi : A →L[ℂ] ℂ) (hphi : phi ∈ stateSpace A) (a : A) :30 inner ℂ (stateGNSVector phi hphi)31 ((positiveLinearMapOfMemStateSpace phi hphi).gnsStarAlgHom a32 (stateGNSVector phi hphi)) = phi a := by33 exact _root_.PositiveLinearMap.inner_gnsCyclicVector_gnsStarAlgHom _ a3435/-- The represented algebraic orbit of the canonical state vector is dense. -/36theorem denseRange_gnsStarAlgHom_stateGNSVector37 (phi : A →L[ℂ] ℂ) (hphi : phi ∈ stateSpace A) :38 DenseRange (fun a : A ↦39 (positiveLinearMapOfMemStateSpace phi hphi).gnsStarAlgHom a40 (stateGNSVector phi hphi)) :=41 _root_.PositiveLinearMap.denseRange_gnsStarAlgHom_apply_gnsCyclicVector _4243/-- Complex-linearity probe for the state/GNS bridge. -/44theorem inner_gnsStarAlgHom_I_stateGNSVector45 (phi : A →L[ℂ] ℂ) (hphi : phi ∈ stateSpace A) :46 inner ℂ (stateGNSVector phi hphi)47 ((positiveLinearMapOfMemStateSpace phi hphi).gnsStarAlgHom48 ((Complex.I : ℂ) • (1 : A)) (stateGNSVector phi hphi)) = Complex.I :=49 by50 rw [inner_gnsStarAlgHom_stateGNSVector]51 have hone : phi 1 = 1 := hphi.252 simp [hone]5354end MathlibAnnex.CStarAlgebra