Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/PureRoot.lean
Pinned GitHub source · Raw UTF-8 source
Back to Purity of the completed root state
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.GNS2import MathlibAnnex.Analysis.CStarAlgebra.PureStateHomogeneity.KishimotoOzawaSakai34/-!5# Purity of the finite-stage root state67At each matrix stage, a normalized positive functional which takes value one on8the distinguished rank-one projection is forced to be the root vector state.9This gives a direct extreme-point proof, using the positive-functional GNS10Cauchy--Schwarz null-vector lemma rather than finite-dimensional spectral theory.11-/1213set_option autoImplicit false1415open Set16open scoped ComplexOrder Convex1718namespace MathlibAnnex.CStarAlgebra.CAR1920@[simp]21theorem rootFunctional_mem_stateSpace (n : ℕ) :22 rootFunctional n ∈ MathlibAnnex.CStarAlgebra.stateSpace (Stage n) := by23 constructor24 · intro x hx25 exact rootLinear_nonneg n x hx26 · exact rootPositiveFunctional_one n2728/-- 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 := by33 let p : Stage n := rootProjection n34 let q : Stage n := 1 - p35 have hp_proj : IsStarProjection p := isStarProjection_rootProjection n36 have hq_proj : IsStarProjection q := hp_proj.one_sub37 let f : Stage n →ₚ[ℂ] ℂ := PositiveLinearMap.mk₀ phi.toLinearMap hphi.138 have hf_apply (x : Stage n) : f x = phi x := rfl39 have hq_zero : f q = 0 := by40 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 := by42 rw [hq_proj.isSelfAdjoint.star_eq, hq_proj.isIdempotentElem.eq, hq_zero]43 have hleft (x : Stage n) : f (q * x) = 0 := by44 simpa [hq_proj.isSelfAdjoint.star_eq] using45 f.apply_star_mul_eq_zero_of_apply_star_mul_self_eq_zero hq_null x46 have hright (x : Stage n) : f (x * q) = 0 := by47 simpa using48 f.apply_star_mul_eq_zero_of_apply_star_mul_self_eq_zero_right hq_null (star x)49 apply ContinuousLinearMap.ext50 intro x51 have hx_decomp : x = p * x * p + q * x + p * x * q := by52 dsimp only [q]53 noncomm_ring [hp_proj.isIdempotentElem.eq]54 calc55 phi x = f x := rfl56 _ = 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 by59 exact rootProjection_mul_mul n x]60 _ = x 0 0 := by simp [map_smul, hf_apply, p, hp]61 _ = rootFunctional n x := rfl6263/-- The distinguished root-coordinate state is pure at every finite matrix stage. -/64theorem isPureState_rootFunctional (n : ℕ) :65 MathlibAnnex.CStarAlgebra.IsPureState (Stage n) (rootFunctional n) := by66 rw [MathlibAnnex.CStarAlgebra.IsPureState, mem_extremePoints_iff_left]67 refine ⟨rootFunctional_mem_stateSpace n, ?_⟩68 intro phi₁ hphi₁ phi₂ hphi₂ hsegment69 rcases hsegment with ⟨a, b, ha, hb, hab, hcomb⟩70 let p : Stage n := rootProjection n71 let q : Stage n := 1 - p72 have hp_proj : IsStarProjection p := isStarProjection_rootProjection n73 have hq_nonneg : 0 ≤ q := hp_proj.one_sub.nonneg74 have hphi₁q : 0 ≤ phi₁ q := hphi₁.1 q hq_nonneg75 have hphi₂q : 0 ≤ phi₂ q := hphi₂.1 q hq_nonneg76 have hrootq : rootFunctional n q = 0 := by77 simp [q, p, rootProjection]78 have hsum : a • phi₁ q + b • phi₂ q = 0 := by79 have := congrArg (fun psi : Stage n →L[ℂ] ℂ => psi q) hcomb80 simpa [hrootq] using this81 have ha_nonneg : 0 ≤ a • phi₁ q := smul_nonneg ha.le hphi₁q82 have hb_nonneg : 0 ≤ b • phi₂ q := smul_nonneg hb.le hphi₂q83 have ha_nonpos : a • phi₁ q ≤ 0 := by84 rw [← hsum]85 simp only [le_add_iff_nonneg_right]86 exact hb_nonneg87 have ha_zero : a • phi₁ q = 0 := le_antisymm ha_nonpos ha_nonneg88 have hphi₁q_zero : phi₁ q = 0 := by89 exact (smul_eq_zero.mp ha_zero).resolve_left ha.ne'90 have hphi₁p : phi₁ p = 1 := by91 have h := hphi₁q_zero92 rw [show q = 1 - p by rfl, map_sub, hphi₁.2, sub_eq_zero] at h93 exact h.symm94 exact eq_rootFunctional_of_apply_rootProjection_eq_one n phi₁ hphi₁ hphi₁p9596end MathlibAnnex.CStarAlgebra.CAR