MathlibAnnex.CStarAlgebra.norm_stateGNSVector

Exact source: MathlibAnnex/Analysis/CStarAlgebra/PureStateGNS/State.lean, lines 22–25.

Raw UTF-8 source

Back to Pure CAR states admit two-sided inner intertwining sequences

1import MathlibAnnex.Analysis.CStarAlgebra.GNS.Adapters
2import MathlibAnnex.Analysis.CStarAlgebra.PureStateHomogeneity.KishimotoOzawaSakai
3
4/-! Canonical GNS data supplied by an ordinary normalized positive state. -/
5
6set_option autoImplicit false
7
8open Set
9
10namespace MathlibAnnex.CStarAlgebra
11
12universe u
13
14variable {A : Type u} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]
15
16/-- The canonical vector of the GNS representation associated to a member of
17`stateSpace`. -/
18noncomputable def stateGNSVector (phi : A →L[ℂ] ℂ) (hphi : phi ∈ stateSpace A) :
19    (positiveLinearMapOfMemStateSpace phi hphi).GNS :=
20  _root_.PositiveLinearMap.gnsCyclicVector (positiveLinearMapOfMemStateSpace phi hphi)
21
22theorem norm_stateGNSVector (phi : A →L[ℂ] ℂ) (hphi : phi ∈ stateSpace A) :
23    ‖stateGNSVector phi hphi‖ = 1 :=
24  _root_.PositiveLinearMap.norm_gnsCyclicVector _
25    (positiveLinearMapOfMemStateSpace_one phi hphi)
26
27/-- The original state is the vector functional of its canonical GNS vector. -/
28theorem inner_gnsStarAlgHom_stateGNSVector
29    (phi : A →L[ℂ] ℂ) (hphi : phi ∈ stateSpace A) (a : A) :
30    inner ℂ (stateGNSVector phi hphi)
31      ((positiveLinearMapOfMemStateSpace phi hphi).gnsStarAlgHom a
32        (stateGNSVector phi hphi)) = phi a := by
33  exact _root_.PositiveLinearMap.inner_gnsCyclicVector_gnsStarAlgHom _ a
34
35/-- The represented algebraic orbit of the canonical state vector is dense. -/
36theorem denseRange_gnsStarAlgHom_stateGNSVector
37    (phi : A →L[ℂ] ℂ) (hphi : phi ∈ stateSpace A) :
38    DenseRange (fun a : A ↦
39      (positiveLinearMapOfMemStateSpace phi hphi).gnsStarAlgHom a
40        (stateGNSVector phi hphi)) :=
41  _root_.PositiveLinearMap.denseRange_gnsStarAlgHom_apply_gnsCyclicVector _
42
43/-- Complex-linearity probe for the state/GNS bridge. -/
44theorem inner_gnsStarAlgHom_I_stateGNSVector
45    (phi : A →L[ℂ] ℂ) (hphi : phi ∈ stateSpace A) :
46    inner ℂ (stateGNSVector phi hphi)
47      ((positiveLinearMapOfMemStateSpace phi hphi).gnsStarAlgHom
48        ((Complex.I : ℂ) • (1 : A)) (stateGNSVector phi hphi)) = Complex.I :=
49  by
50    rw [inner_gnsStarAlgHom_stateGNSVector]
51    have hone : phi 1 = 1 := hphi.2
52    simp [hone]
53
54end MathlibAnnex.CStarAlgebra