Exact source: MathlibAnnex/Analysis/CStarAlgebra/State/Purity.lean
Pinned GitHub source · Raw UTF-8 source
Back to The GNS representation of a pure state is irreducible
1import MathlibAnnex.Analysis.CStarAlgebra.State.Basic23/-!4# Pure states and dominated positive functionals56The proof is the elementary convex-cone part of the pure-state/GNS bridge.7-/89set_option autoImplicit false1011open Set12open scoped ComplexOrder Convex1314namespace MathlibAnnex.Analysis.CStarAlgebra1516universe u1718variable {A : Type u} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]1920/-- A positive continuous functional which vanishes at one is zero. -/21theorem continuousLinearMap_eq_zero_of_nonnegative_of_one_eq_zero22 (rho : A →L[ℂ] ℂ) (hrho : ∀ a : A, 0 ≤ a → 0 ≤ rho a)23 (hrho_one : rho 1 = 0) : rho = 0 := by24 let f : A →ₚ[ℂ] ℂ := PositiveLinearMap.mk₀ rho.toLinearMap hrho25 have hf_one : f 1 = 0 := hrho_one26 have hf_zero_of_nonneg (a : A) (ha : 0 ≤ a) : f a = 0 := by27 apply norm_eq_zero.mp28 apply le_antisymm29 · simpa [hf_one] using f.norm_apply_le_of_nonneg a ha30 · exact norm_nonneg _31 apply ContinuousLinearMap.ext32 intro a33 obtain ⟨x, hx_nonneg, -, ha⟩ := CStarAlgebra.exists_sum_four_nonneg a34 change f a = 035 rw [ha, map_sum]36 simp [hf_zero_of_nonneg, hx_nonneg]3738/-- A positive functional dominated by a pure state is a real scalar multiple39of that state. -/40theorem eq_smul_of_pureState_of_nonnegative_le41 (phi rho : A →L[ℂ] ℂ) (hphi : IsPureState A phi)42 (hrho : ∀ a : A, 0 ≤ a → 0 ≤ rho a)43 (hle : ∀ a : A, 0 ≤ a → rho a ≤ phi a) :44 ∃ t : ℝ, 0 ≤ t ∧ t ≤ 1 ∧ rho = t • phi := by45 rw [IsPureState, mem_extremePoints_iff_left] at hphi46 obtain ⟨t, ht, ht_eq⟩ := RCLike.nonneg_iff_exists_ofReal.mp47 (hrho 1 (by simpa using star_mul_self_nonneg (1 : A)))48 have ht_le_one : t ≤ 1 := by49 have h := hle 1 (by simpa using star_mul_self_nonneg (1 : A))50 rw [hphi.1.2] at h51 have hre := (RCLike.nonneg_iff.mp (sub_nonneg.mpr h)).152 have ht_re : (rho 1).re = t := by53 simpa using congrArg Complex.re ht_eq.symm54 simpa [ht_re] using hre55 by_cases ht_zero : t = 056 · refine ⟨t, ht, ht_le_one, ?_⟩57 have hrho_one : rho 1 = 0 := by simpa [ht_zero] using ht_eq.symm58 rw [continuousLinearMap_eq_zero_of_nonnegative_of_one_eq_zero rho hrho hrho_one,59 ht_zero]60 exact (zero_smul ℝ phi).symm61 by_cases ht_one : t = 162 · refine ⟨t, ht, ht_le_one, ?_⟩63 have hdiff_nonneg : ∀ a : A, 0 ≤ a → 0 ≤ (phi - rho) a := by64 intro a ha65 simpa using sub_nonneg.mpr (hle a ha)66 have hdiff_one : (phi - rho) 1 = 0 := by67 simp [hphi.1.2, ← ht_eq, ht_one]68 have hdiff := continuousLinearMap_eq_zero_of_nonnegative_of_one_eq_zero69 (phi - rho) hdiff_nonneg hdiff_one70 rw [ht_one, one_smul]71 exact (sub_eq_zero.mp hdiff).symm72 have ht_pos : 0 < t := lt_of_le_of_ne ht (Ne.symm ht_zero)73 have ht_lt_one : t < 1 := lt_of_le_of_ne ht_le_one ht_one74 have htC : (t : ℂ) ≠ 0 := by exact_mod_cast ht_pos.ne'75 have hsubC : (1 - (t : ℂ)) ≠ 0 := by76 exact_mod_cast sub_ne_zero.mpr (Ne.symm ht_one)77 let psi : A →L[ℂ] ℂ := t⁻¹ • rho78 let chi : A →L[ℂ] ℂ := (1 - t)⁻¹ • (phi - rho)79 have hpsi : psi ∈ stateSpace A := by80 constructor81 · intro a ha82 dsimp [psi]83 exact smul_nonneg (inv_nonneg.mpr ht.le) (hrho a ha)84 · dsimp [psi]85 rw [ContinuousLinearMap.smul_apply, ← ht_eq]86 simpa [ht_pos.ne']87 have hchi : chi ∈ stateSpace A := by88 constructor89 · intro a ha90 dsimp [chi]91 exact smul_nonneg (inv_nonneg.mpr (sub_nonneg.mpr ht_le_one))92 (sub_nonneg.mpr (hle a ha))93 · dsimp [chi]94 rw [ContinuousLinearMap.smul_apply, ContinuousLinearMap.sub_apply,95 hphi.1.2, ← ht_eq]96 rw [Complex.real_smul]97 push_cast98 exact inv_mul_cancel₀ hsubC99 have hsegment : phi ∈ openSegment ℝ psi chi := by100 refine ⟨t, 1 - t, ht_pos, sub_pos.mpr ht_lt_one, by ring, ?_⟩101 apply ContinuousLinearMap.ext102 intro a103 dsimp [psi, chi]104 simp only [ContinuousLinearMap.add_apply, ContinuousLinearMap.smul_apply,105 ContinuousLinearMap.sub_apply]106 simp only [Complex.real_smul]107 push_cast108 simp [htC, hsubC]109 have hpsi_eq : psi = phi := hphi.2 psi hpsi chi hchi hsegment110 refine ⟨t, ht, ht_le_one, ?_⟩111 calc112 rho = t • psi := by113 apply ContinuousLinearMap.ext114 intro a115 dsimp [psi]116 simp [ht_pos.ne']117 _ = t • phi := congrArg (t • ·) hpsi_eq118119end MathlibAnnex.Analysis.CStarAlgebra