Exact source: MathlibAnnex/Analysis/CStarAlgebra/PureStateHomogeneity/KishimotoOzawaSakai.lean
Pinned GitHub source · Raw UTF-8 source
Back to Approximately inner homogeneity of pure CAR states
1import Mathlib.Algebra.Star.Unitary2import Mathlib.Analysis.Convex.Extreme3import Mathlib.Analysis.CStarAlgebra.PositiveLinearMap4import Mathlib.RingTheory.TwoSidedIdeal.Basic5import Mathlib.Topology.Bases67/-!8# Conditional KOS boundary910This file defines the one external mathematical proposition used by the source11construction. It introduces no global postulate.12-/1314set_option autoImplicit false1516open Set17open scoped ComplexOrder1819namespace MathlibAnnex.CStarAlgebra2021universe u2223/-- 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}2728/-- Rebundle a member of the state space as Mathlib's positive linear map,29the input expected by the existing GNS construction. -/30def positiveLinearMapOfMemStateSpace31 {A : Type u} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]32 (phi : A →L[ℂ] ℂ) (hphi : phi ∈ stateSpace A) : A →ₚ[ℂ] ℂ where33 toLinearMap := phi.toLinearMap34 monotone' := by35 intro a b hab36 apply sub_nonneg.mp37 change 0 ≤ phi b - phi a38 rw [← map_sub]39 exact hphi.1 (b - a) (sub_nonneg.mpr hab)4041@[simp]42theorem positiveLinearMapOfMemStateSpace_apply43 {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 rfl4748@[simp]49theorem positiveLinearMapOfMemStateSpace_one50 {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.25455/-- 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 ℝ5960/-- 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 = ⊤6465/-- The unital-simple approximately-inner consequence of KOS used here.66The state equation is `phi ∘ alpha = psi`; approximation is point-norm with67one 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)‖ < epsilon7879end MathlibAnnex.CStarAlgebra