Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/Trace.lean
Pinned GitHub source · Raw UTF-8 source
Back to Constructing the normalized trace on the completed CAR algebra
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.Completion2import MathlibAnnex.Analysis.CStarAlgebra.CAR.FiniteTrace3import MathlibAnnex.Analysis.CStarAlgebra.State.Basic45/-!6# The normalized trace on the completed CAR algebra78The compatible finite traces are first defined on the actual algebraic9inductive limit, transported to the metric union, and continuously extended10to its completion. Positivity, traciality and normalization are all proved.11-/1213set_option autoImplicit false1415open scoped ComplexOrder1617namespace MathlibAnnex.CStarAlgebra.CAR1819@[simp]20theorem stageTrace_embed (n : ℕ) : ∀ (m : ℕ) (h : n ≤ m) (a : Stage n),21 stageTrace m (embed n m h a) = stageTrace n a := by22 apply Nat.le_induction23 · intro a24 rw [embed_refl]25 rfl26 · intro m h ih a27 rw [embed_succ, StarAlgHom.comp_apply, stageTrace_step, ih]28 exact h2930/-- 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)3536@[simp]37theorem algTraceLinear_algStageHom (n : ℕ) (a : Stage n) :38 algTraceLinear (algStageHom n a) = stageTrace n a := rfl3940/-- The trace on the normed, not yet completed, union. -/41noncomputable def preTraceLinear : PreCAR →ₗ[ℂ] ℂ :=42 algTraceLinear.comp preStarAlgEquiv.toAlgEquiv.toLinearEquiv.toLinearMap4344@[simp]45theorem preTraceLinear_stageHom (n : ℕ) (a : Stage n) :46 preTraceLinear (stageHom n a) = stageTrace n a := rfl4748theorem norm_preTraceLinear_le (x : PreCAR) : ‖preTraceLinear x‖ ≤ ‖x‖ := by49 obtain ⟨n, a, _, ha, _⟩ := exists_common_stage x x50 rw [← ha, preTraceLinear_stageHom, norm_stageHom]51 exact norm_stageTrace_le n a5253/-- The continuous trace on the metric union. -/54noncomputable def preTrace : PreCAR →L[ℂ] ℂ :=55 preTraceLinear.mkContinuous 1 fun x ↦ by56 simpa only [one_mul] using norm_preTraceLinear_le x5758@[simp]59theorem preTrace_stageHom (n : ℕ) (a : Stage n) :60 preTrace (stageHom n a) = stageTrace n a := rfl6162/-- The normalized trace of the completed CAR algebra. -/63noncomputable def trace : Limit →L[ℂ] ℂ :=64 preTrace.extend (UniformSpace.Completion.toComplL : PreCAR →L[ℂ] Limit)6566@[simp]67theorem trace_coe (x : PreCAR) : trace (x : Limit) = preTrace x :=68 ContinuousLinearMap.extend_eq preTrace UniformSpace.Completion.denseRange_coe69 (UniformSpace.Completion.isUniformInducing_coe PreCAR) x7071@[simp]72theorem trace_ofStage (n : ℕ) (a : Stage n) : trace (ofStage n a) = stageTrace n a := by73 rw [ofStage_apply, trace_coe, preTrace_stageHom]7475theorem norm_trace_le (x : Limit) : ‖trace x‖ ≤ ‖x‖ := by76 refine UniformSpace.Completion.induction_on (α := PreCAR)77 (p := fun x ↦ ‖trace x‖ ≤ ‖x‖) x ?_ ?_78 · exact isClosed_le trace.continuous.norm continuous_norm79 · intro a80 rw [trace_coe, UniformSpace.Completion.norm_coe]81 change ‖preTraceLinear a‖ ≤ ‖a‖82 exact norm_preTraceLinear_le a8384@[simp]85theorem trace_one : trace 1 = 1 := by86 calc87 trace 1 = trace (ofStage 0 (1 : Stage 0)) :=88 congrArg trace ((ofStage 0).map_one).symm89 _ = stageTrace 0 1 := trace_ofStage 0 190 _ = 1 := stageTrace_one 09192private theorem preTrace_star_mul_self_nonneg (x : PreCAR) :93 0 ≤ preTrace (star x * x) := by94 obtain ⟨n, a, _, ha, _⟩ := exists_common_stage x x95 rw [← ha, ← map_star, ← map_mul, preTrace_stageHom]96 exact stageTrace_star_mul_self_nonneg n a9798theorem trace_star_mul_self_nonneg (x : Limit) : 0 ≤ trace (star x * x) := by99 refine UniformSpace.Completion.induction_on (α := PreCAR)100 (p := fun x ↦ 0 ≤ trace (star x * x)) x ?_ ?_101 · exact isClosed_le continuous_const102 (trace.continuous.comp (continuous_limit_star.mul continuous_id))103 · intro a104 simpa only [← UniformSpace.Completion.coe_mul, star_coe, trace_coe] using105 preTrace_star_mul_self_nonneg a106107theorem trace_nonneg (x : Limit) (hx : 0 ≤ x) : 0 ≤ trace x := by108 obtain ⟨y, rfl⟩ := CStarAlgebra.nonneg_iff_eq_star_mul_self.mp hx109 exact trace_star_mul_self_nonneg y110111theorem trace_mem_stateSpace :112 trace ∈ MathlibAnnex.Analysis.CStarAlgebra.stateSpace Limit :=113 ⟨trace_nonneg, trace_one⟩114115private theorem preTrace_mul_comm (x y : PreCAR) : preTrace (x * y) = preTrace (y * x) := by116 obtain ⟨n, a, b, ha, hb⟩ := exists_common_stage x y117 rw [← ha, ← hb, ← map_mul, ← map_mul, preTrace_stageHom, preTrace_stageHom]118 exact stageTrace_mul_comm n a b119120theorem trace_mul_comm (x y : Limit) : trace (x * y) = trace (y * x) := by121 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_prop124 · intro a b125 simpa only [← UniformSpace.Completion.coe_mul, trace_coe] using preTrace_mul_comm a b126127@[simp]128theorem trace_rootFlag (n : ℕ) : trace (rootFlag n) = (2 ^ n : ℂ)⁻¹ := by129 rw [rootFlag, trace_ofStage, stageTrace_rootProjection]130131/-- The same trace as a positive linear map, for GNS calculations. -/132noncomputable def tracePositive : Limit →ₚ[ℂ] ℂ :=133 PositiveLinearMap.mk₀ trace.toLinearMap trace_nonneg134135@[simp]136theorem tracePositive_apply (x : Limit) : tracePositive x = trace x := rfl137138@[simp]139theorem tracePositive_one : tracePositive 1 = 1 := trace_one140141end MathlibAnnex.CStarAlgebra.CAR