Exact source: MathlibAnnex/Analysis/CStarAlgebra/PureStateHomogeneity/KishimotoOzawaSakai.lean, lines 67–79.
Back to Approximately inner homogeneity of pure CAR states
1import Mathlib.Algebra.Star.Unitary 2import Mathlib.Analysis.Convex.Extreme 3import Mathlib.Analysis.CStarAlgebra.PositiveLinearMap 4import Mathlib.RingTheory.TwoSidedIdeal.Basic 5import Mathlib.Topology.Bases 6 7/-! 8# Conditional KOS boundary 9 10This file defines the one external mathematical proposition used by the source 11construction. It introduces no global postulate. 12-/ 13 14set_option autoImplicit false 15 16open Set 17open scoped ComplexOrder 18 19namespace MathlibAnnex.CStarAlgebra 20 21universe u 22 23/-- Normalized positive continuous complex-linear functionals. -/ 24def stateSpace (A : Type u) [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] : 25 Set (A →L[ℂ] ℂ) := 26 {phi | (∀ a : A, 0 ≤ a → 0 ≤ phi a) ∧ phi 1 = 1} 27 28/-- Rebundle a member of the state space as Mathlib's positive linear map, 29the input expected by the existing GNS construction. -/ 30def positiveLinearMapOfMemStateSpace 31 {A : Type u} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] 32 (phi : A →L[ℂ] ℂ) (hphi : phi ∈ stateSpace A) : A →ₚ[ℂ] ℂ where 33 toLinearMap := phi.toLinearMap 34 monotone' := by 35 intro a b hab 36 apply sub_nonneg.mp 37 change 0 ≤ phi b - phi a 38 rw [← map_sub] 39 exact hphi.1 (b - a) (sub_nonneg.mpr hab) 40 41@[simp] 42theorem positiveLinearMapOfMemStateSpace_apply 43 {A : Type u} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] 44 (phi : A →L[ℂ] ℂ) (hphi : phi ∈ stateSpace A) (a : A) : 45 positiveLinearMapOfMemStateSpace phi hphi a = phi a := 46 rfl 47 48@[simp] 49theorem positiveLinearMapOfMemStateSpace_one 50 {A : Type u} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] 51 (phi : A →L[ℂ] ℂ) (hphi : phi ∈ stateSpace A) : 52 positiveLinearMapOfMemStateSpace phi hphi 1 = 1 := 53 hphi.2 54 55/-- A pure state is an extreme point of the ordinary state space. -/ 56def IsPureState (A : Type u) [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] 57 (phi : A →L[ℂ] ℂ) : Prop := 58 phi ∈ (stateSpace A).extremePoints ℝ 59 60/-- Simplicity with respect to norm-closed two-sided ideals. -/ 61def IsSimpleCStarAlgebra (A : Type u) [CStarAlgebra A] : Prop := 62 Nontrivial A ∧ 63 ∀ I : TwoSidedIdeal A, IsClosed (I : Set A) → I = ⊥ ∨ I = ⊤ 64 65/-- The unital-simple approximately-inner consequence of KOS used here. 66The state equation is `phi ∘ alpha = psi`; approximation is point-norm with 67one unitary simultaneously serving every element of the finite set. -/ 68def KishimotoOzawaSakaiProperty : Prop := 69 ∀ (A : Type u) [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] 70 [TopologicalSpace.SeparableSpace A], 71 IsSimpleCStarAlgebra A → 72 ∀ (phi psi : A →L[ℂ] ℂ), IsPureState A phi → IsPureState A psi → 73 ∃ alpha : A ≃⋆ₐ[ℂ] A, 74 (∀ a : A, phi (alpha a) = psi a) ∧ 75 ∀ (F : Finset A) (epsilon : ℝ), 0 < epsilon → 76 ∃ v : unitary A, ∀ a ∈ F, 77 ‖alpha a - (v : A) * a * star (v : A)‖ < epsilon 78 79end MathlibAnnex.CStarAlgebra