Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/PureRoot.lean, lines 63–94.
Back to Purity of the completed root state
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.GNS 2import MathlibAnnex.Analysis.CStarAlgebra.PureStateHomogeneity.KishimotoOzawaSakai 3 4/-! 5# Purity of the finite-stage root state 6 7At each matrix stage, a normalized positive functional which takes value one on 8the distinguished rank-one projection is forced to be the root vector state. 9This gives a direct extreme-point proof, using the positive-functional GNS 10Cauchy--Schwarz null-vector lemma rather than finite-dimensional spectral theory. 11-/ 12 13set_option autoImplicit false 14 15open Set 16open scoped ComplexOrder Convex 17 18namespace MathlibAnnex.CStarAlgebra.CAR 19 20@[simp] 21theorem rootFunctional_mem_stateSpace (n : ℕ) : 22 rootFunctional n ∈ MathlibAnnex.CStarAlgebra.stateSpace (Stage n) := by 23 constructor 24 · intro x hx 25 exact rootLinear_nonneg n x hx 26 · exact rootPositiveFunctional_one n 27 28/-- A state supported with value one on the root projection is the root state. -/ 29theorem eq_rootFunctional_of_apply_rootProjection_eq_one (n : ℕ) 30 (phi : Stage n →L[ℂ] ℂ) (hphi : phi ∈ MathlibAnnex.CStarAlgebra.stateSpace (Stage n)) 31 (hp : phi (rootProjection n) = 1) : 32 phi = rootFunctional n := by 33 let p : Stage n := rootProjection n 34 let q : Stage n := 1 - p 35 have hp_proj : IsStarProjection p := isStarProjection_rootProjection n 36 have hq_proj : IsStarProjection q := hp_proj.one_sub 37 let f : Stage n →ₚ[ℂ] ℂ := PositiveLinearMap.mk₀ phi.toLinearMap hphi.1 38 have hf_apply (x : Stage n) : f x = phi x := rfl 39 have hq_zero : f q = 0 := by 40 rw [hf_apply, show q = 1 - p by rfl, map_sub, hphi.2, hp, sub_self] 41 have hq_null : f (star q * q) = 0 := by 42 rw [hq_proj.isSelfAdjoint.star_eq, hq_proj.isIdempotentElem.eq, hq_zero] 43 have hleft (x : Stage n) : f (q * x) = 0 := by 44 simpa [hq_proj.isSelfAdjoint.star_eq] using 45 f.apply_star_mul_eq_zero_of_apply_star_mul_self_eq_zero hq_null x 46 have hright (x : Stage n) : f (x * q) = 0 := by 47 simpa using 48 f.apply_star_mul_eq_zero_of_apply_star_mul_self_eq_zero_right hq_null (star x) 49 apply ContinuousLinearMap.ext 50 intro x 51 have hx_decomp : x = p * x * p + q * x + p * x * q := by 52 dsimp only [q] 53 noncomm_ring [hp_proj.isIdempotentElem.eq] 54 calc 55 phi x = f x := rfl 56 _ = f (p * x * p + q * x + p * x * q) := by rw [← hx_decomp] 57 _ = f (p * x * p) := by rw [map_add, map_add, hleft, hright, add_zero, add_zero] 58 _ = f ((x 0 0) • p) := by rw [show p * x * p = (x 0 0) • p by 59 exact rootProjection_mul_mul n x] 60 _ = x 0 0 := by simp [map_smul, hf_apply, p, hp] 61 _ = rootFunctional n x := rfl 62 63/-- The distinguished root-coordinate state is pure at every finite matrix stage. -/ 64theorem isPureState_rootFunctional (n : ℕ) : 65 MathlibAnnex.CStarAlgebra.IsPureState (Stage n) (rootFunctional n) := by 66 rw [MathlibAnnex.CStarAlgebra.IsPureState, mem_extremePoints_iff_left] 67 refine ⟨rootFunctional_mem_stateSpace n, ?_⟩ 68 intro phi₁ hphi₁ phi₂ hphi₂ hsegment 69 rcases hsegment with ⟨a, b, ha, hb, hab, hcomb⟩ 70 let p : Stage n := rootProjection n 71 let q : Stage n := 1 - p 72 have hp_proj : IsStarProjection p := isStarProjection_rootProjection n 73 have hq_nonneg : 0 ≤ q := hp_proj.one_sub.nonneg 74 have hphi₁q : 0 ≤ phi₁ q := hphi₁.1 q hq_nonneg 75 have hphi₂q : 0 ≤ phi₂ q := hphi₂.1 q hq_nonneg 76 have hrootq : rootFunctional n q = 0 := by 77 simp [q, p, rootProjection] 78 have hsum : a • phi₁ q + b • phi₂ q = 0 := by 79 have := congrArg (fun psi : Stage n →L[ℂ] ℂ => psi q) hcomb 80 simpa [hrootq] using this 81 have ha_nonneg : 0 ≤ a • phi₁ q := smul_nonneg ha.le hphi₁q 82 have hb_nonneg : 0 ≤ b • phi₂ q := smul_nonneg hb.le hphi₂q 83 have ha_nonpos : a • phi₁ q ≤ 0 := by 84 rw [← hsum] 85 simp only [le_add_iff_nonneg_right] 86 exact hb_nonneg 87 have ha_zero : a • phi₁ q = 0 := le_antisymm ha_nonpos ha_nonneg 88 have hphi₁q_zero : phi₁ q = 0 := by 89 exact (smul_eq_zero.mp ha_zero).resolve_left ha.ne' 90 have hphi₁p : phi₁ p = 1 := by 91 have h := hphi₁q_zero 92 rw [show q = 1 - p by rfl, map_sub, hphi₁.2, sub_eq_zero] at h 93 exact h.symm 94 exact eq_rootFunctional_of_apply_rootProjection_eq_one n phi₁ hphi₁ hphi₁p 95 96end MathlibAnnex.CStarAlgebra.CAR