Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/Trace.lean, lines 98–105.
Back to Constructing the normalized trace on the completed CAR algebra
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.Completion 2import MathlibAnnex.Analysis.CStarAlgebra.CAR.FiniteTrace 3import MathlibAnnex.Analysis.CStarAlgebra.State.Basic 4 5/-! 6# The normalized trace on the completed CAR algebra 7 8The compatible finite traces are first defined on the actual algebraic 9inductive limit, transported to the metric union, and continuously extended 10to its completion. Positivity, traciality and normalization are all proved. 11-/ 12 13set_option autoImplicit false 14 15open scoped ComplexOrder 16 17namespace MathlibAnnex.CStarAlgebra.CAR 18 19@[simp] 20theorem stageTrace_embed (n : ℕ) : ∀ (m : ℕ) (h : n ≤ m) (a : Stage n), 21 stageTrace m (embed n m h a) = stageTrace n a := by 22 apply Nat.le_induction 23 · intro a 24 rw [embed_refl] 25 rfl 26 · intro m h ih a 27 rw [embed_succ, StarAlgHom.comp_apply, stageTrace_step, ih] 28 exact h 29 30/-- The trace on the algebraic inductive limit. -/ 31noncomputable def algTraceLinear : AlgCAR →ₗ[ℂ] ℂ := 32 DirectLimit.Module.lift ℂ ℕ Stage (fun _ _ h ↦ embed _ _ h) 33 (fun n ↦ (stageTrace n).toLinearMap) 34 (fun i j hij a ↦ stageTrace_embed i j hij a) 35 36@[simp] 37theorem algTraceLinear_algStageHom (n : ℕ) (a : Stage n) : 38 algTraceLinear (algStageHom n a) = stageTrace n a := rfl 39 40/-- The trace on the normed, not yet completed, union. -/ 41noncomputable def preTraceLinear : PreCAR →ₗ[ℂ] ℂ := 42 algTraceLinear.comp preStarAlgEquiv.toAlgEquiv.toLinearEquiv.toLinearMap 43 44@[simp] 45theorem preTraceLinear_stageHom (n : ℕ) (a : Stage n) : 46 preTraceLinear (stageHom n a) = stageTrace n a := rfl 47 48theorem norm_preTraceLinear_le (x : PreCAR) : ‖preTraceLinear x‖ ≤ ‖x‖ := by 49 obtain ⟨n, a, _, ha, _⟩ := exists_common_stage x x 50 rw [← ha, preTraceLinear_stageHom, norm_stageHom] 51 exact norm_stageTrace_le n a 52 53/-- The continuous trace on the metric union. -/ 54noncomputable def preTrace : PreCAR →L[ℂ] ℂ := 55 preTraceLinear.mkContinuous 1 fun x ↦ by 56 simpa only [one_mul] using norm_preTraceLinear_le x 57 58@[simp] 59theorem preTrace_stageHom (n : ℕ) (a : Stage n) : 60 preTrace (stageHom n a) = stageTrace n a := rfl 61 62/-- The normalized trace of the completed CAR algebra. -/ 63noncomputable def trace : Limit →L[ℂ] ℂ := 64 preTrace.extend (UniformSpace.Completion.toComplL : PreCAR →L[ℂ] Limit) 65 66@[simp] 67theorem trace_coe (x : PreCAR) : trace (x : Limit) = preTrace x := 68 ContinuousLinearMap.extend_eq preTrace UniformSpace.Completion.denseRange_coe 69 (UniformSpace.Completion.isUniformInducing_coe PreCAR) x 70 71@[simp] 72theorem trace_ofStage (n : ℕ) (a : Stage n) : trace (ofStage n a) = stageTrace n a := by 73 rw [ofStage_apply, trace_coe, preTrace_stageHom] 74 75theorem norm_trace_le (x : Limit) : ‖trace x‖ ≤ ‖x‖ := by 76 refine UniformSpace.Completion.induction_on (α := PreCAR) 77 (p := fun x ↦ ‖trace x‖ ≤ ‖x‖) x ?_ ?_ 78 · exact isClosed_le trace.continuous.norm continuous_norm 79 · intro a 80 rw [trace_coe, UniformSpace.Completion.norm_coe] 81 change ‖preTraceLinear a‖ ≤ ‖a‖ 82 exact norm_preTraceLinear_le a 83 84@[simp] 85theorem trace_one : trace 1 = 1 := by 86 calc 87 trace 1 = trace (ofStage 0 (1 : Stage 0)) := 88 congrArg trace ((ofStage 0).map_one).symm 89 _ = stageTrace 0 1 := trace_ofStage 0 1 90 _ = 1 := stageTrace_one 0 91 92private theorem preTrace_star_mul_self_nonneg (x : PreCAR) : 93 0 ≤ preTrace (star x * x) := by 94 obtain ⟨n, a, _, ha, _⟩ := exists_common_stage x x 95 rw [← ha, ← map_star, ← map_mul, preTrace_stageHom] 96 exact stageTrace_star_mul_self_nonneg n a 97 98theorem trace_star_mul_self_nonneg (x : Limit) : 0 ≤ trace (star x * x) := by 99 refine UniformSpace.Completion.induction_on (α := PreCAR) 100 (p := fun x ↦ 0 ≤ trace (star x * x)) x ?_ ?_ 101 · exact isClosed_le continuous_const 102 (trace.continuous.comp (continuous_limit_star.mul continuous_id)) 103 · intro a 104 simpa only [← UniformSpace.Completion.coe_mul, star_coe, trace_coe] using 105 preTrace_star_mul_self_nonneg a 106 107theorem trace_nonneg (x : Limit) (hx : 0 ≤ x) : 0 ≤ trace x := by 108 obtain ⟨y, rfl⟩ := CStarAlgebra.nonneg_iff_eq_star_mul_self.mp hx 109 exact trace_star_mul_self_nonneg y 110 111theorem trace_mem_stateSpace : 112 trace ∈ MathlibAnnex.Analysis.CStarAlgebra.stateSpace Limit := 113 ⟨trace_nonneg, trace_one⟩ 114 115private theorem preTrace_mul_comm (x y : PreCAR) : preTrace (x * y) = preTrace (y * x) := by 116 obtain ⟨n, a, b, ha, hb⟩ := exists_common_stage x y 117 rw [← ha, ← hb, ← map_mul, ← map_mul, preTrace_stageHom, preTrace_stageHom] 118 exact stageTrace_mul_comm n a b 119 120theorem trace_mul_comm (x y : Limit) : trace (x * y) = trace (y * x) := by 121 refine UniformSpace.Completion.induction_on₂ (α := PreCAR) (β := PreCAR) 122 (p := fun x y ↦ trace (x * y) = trace (y * x)) x y ?_ ?_ 123 · apply isClosed_eq <;> fun_prop 124 · intro a b 125 simpa only [← UniformSpace.Completion.coe_mul, trace_coe] using preTrace_mul_comm a b 126 127@[simp] 128theorem trace_rootFlag (n : ℕ) : trace (rootFlag n) = (2 ^ n : ℂ)⁻¹ := by 129 rw [rootFlag, trace_ofStage, stageTrace_rootProjection] 130 131/-- The same trace as a positive linear map, for GNS calculations. -/ 132noncomputable def tracePositive : Limit →ₚ[ℂ] ℂ := 133 PositiveLinearMap.mk₀ trace.toLinearMap trace_nonneg 134 135@[simp] 136theorem tracePositive_apply (x : Limit) : tracePositive x = trace x := rfl 137 138@[simp] 139theorem tracePositive_one : tracePositive 1 = 1 := trace_one 140 141end MathlibAnnex.CStarAlgebra.CAR