Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/TraceFlag.lean, lines 42–46.
Back to Shell matching fixes the trace of transported flags · Back to Transported flags vanish on vectors generated by a trace vector · Back to Pointed unitary transport between trace-cyclic target representations
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.Trace 2import MathlibAnnex.Analysis.CStarAlgebra.CAR.AtomicSource 3import MathlibAnnex.Analysis.CStarAlgebra.GNS.TracialProjection 4import Mathlib.Analysis.SpecificLimits.Normed 5 6/-! 7# Trace of the fixed transported flags 8 9No automorphism is reselected, and no trace-invariance axiom for the chosen 10automorphisms is needed. The exact initial/final shell identities force the 11trace of every transported flag by a finite telescoping induction. 12-/ 13 14set_option autoImplicit false 15 16open Filter Topology 17 18namespace MathlibAnnex.CStarAlgebra.CAR 19 20open MathlibAnnex.Analysis.CStarAlgebra 21 22private theorem trace_transportedFlag_sub (family : RepresentativeShellFamily) 23 (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) (n : ℕ) : 24 trace (transportedFlag family i n) - trace (transportedFlag family i (n + 1)) = 25 trace (rootFlag n) - trace (rootFlag (n + 1)) := by 26 rw [← map_sub, ← map_sub, ← representativeLink_initial family i n, 27 ← representativeLink_final family i n] 28 exact trace_mul_comm _ _ 29 30/-- The trace of a transported flag agrees with the trace of the root flag. -/ 31theorem trace_transportedFlag_eq_trace_rootFlag (family : RepresentativeShellFamily) 32 (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) (n : ℕ) : 33 trace (transportedFlag family i n) = trace (rootFlag n) := by 34 induction n with 35 | zero => rw [transportedFlag_zero, rootFlag_zero] 36 | succ n ih => 37 have h := trace_transportedFlag_sub family i n 38 rw [ih] at h 39 have h' := congrArg (fun z : ℂ ↦ trace (rootFlag n) - z) h 40 simpa only [sub_sub_cancel] using h' 41 42@[simp] 43theorem trace_transportedFlag (family : RepresentativeShellFamily) 44 (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) (n : ℕ) : 45 trace (transportedFlag family i n) = (2 ^ n : ℂ)⁻¹ := by 46 rw [trace_transportedFlag_eq_trace_rootFlag, trace_rootFlag] 47 48private theorem tendsto_inv_pow_two_atTop_nhds_zero : 49 Tendsto (fun n : ℕ ↦ (2 ^ n : ℝ)⁻¹) atTop (nhds 0) := by 50 simp_rw [← inv_pow] 51 exact tendsto_pow_atTop_nhds_zero_of_norm_lt_one (by norm_num) 52 53universe v 54variable {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] 55 56theorem tendsto_rootFlag_orbit_zero (σ : Representation Limit H) (ξ : H) 57 (hξ : ∀ a, Representation.vectorFunctional σ ξ a = trace a) (b : Limit) : 58 Tendsto (fun n ↦ σ (rootFlag n) (σ b ξ)) atTop (nhds 0) := by 59 apply tendsto_projection_orbit_zero tracePositive trace_mul_comm σ ξ hξ 60 rootFlag isStarProjection_rootFlag (fun n ↦ (2 ^ n : ℝ)⁻¹) 61 · intro n 62 simp only [tracePositive_apply, trace_rootFlag, Complex.ofReal_inv, 63 Complex.ofReal_pow, Complex.ofReal_ofNat] 64 · exact tendsto_inv_pow_two_atTop_nhds_zero 65 66theorem tendsto_transportedFlag_orbit_zero (family : RepresentativeShellFamily) 67 (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) 68 (σ : Representation Limit H) (ξ : H) 69 (hξ : ∀ a, Representation.vectorFunctional σ ξ a = trace a) (b : Limit) : 70 Tendsto (fun n ↦ σ (transportedFlag family i n) (σ b ξ)) atTop (nhds 0) := by 71 apply tendsto_projection_orbit_zero tracePositive trace_mul_comm σ ξ hξ 72 (transportedFlag family i) (isStarProjection_transportedFlag family i) 73 (fun n ↦ (2 ^ n : ℝ)⁻¹) 74 · intro n 75 simp only [tracePositive_apply, trace_transportedFlag, Complex.ofReal_inv, 76 Complex.ofReal_pow, Complex.ofReal_ofNat] 77 · exact tendsto_inv_pow_two_atTop_nhds_zero 78 79end MathlibAnnex.CStarAlgebra.CAR