Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/TraceFlag.lean
Pinned GitHub source · Raw UTF-8 source
Back to Transported flags vanish on vectors generated by a trace vector
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.Trace2import MathlibAnnex.Analysis.CStarAlgebra.CAR.AtomicSource3import MathlibAnnex.Analysis.CStarAlgebra.GNS.TracialProjection4import Mathlib.Analysis.SpecificLimits.Normed56/-!7# Trace of the fixed transported flags89No automorphism is reselected, and no trace-invariance axiom for the chosen10automorphisms is needed. The exact initial/final shell identities force the11trace of every transported flag by a finite telescoping induction.12-/1314set_option autoImplicit false1516open Filter Topology1718namespace MathlibAnnex.CStarAlgebra.CAR1920open MathlibAnnex.Analysis.CStarAlgebra2122private 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)) := by26 rw [← map_sub, ← map_sub, ← representativeLink_initial family i n,27 ← representativeLink_final family i n]28 exact trace_mul_comm _ _2930/-- 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) := by34 induction n with35 | zero => rw [transportedFlag_zero, rootFlag_zero]36 | succ n ih =>37 have h := trace_transportedFlag_sub family i n38 rw [ih] at h39 have h' := congrArg (fun z : ℂ ↦ trace (rootFlag n) - z) h40 simpa only [sub_sub_cancel] using h'4142@[simp]43theorem trace_transportedFlag (family : RepresentativeShellFamily)44 (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) (n : ℕ) :45 trace (transportedFlag family i n) = (2 ^ n : ℂ)⁻¹ := by46 rw [trace_transportedFlag_eq_trace_rootFlag, trace_rootFlag]4748private theorem tendsto_inv_pow_two_atTop_nhds_zero :49 Tendsto (fun n : ℕ ↦ (2 ^ n : ℝ)⁻¹) atTop (nhds 0) := by50 simp_rw [← inv_pow]51 exact tendsto_pow_atTop_nhds_zero_of_norm_lt_one (by norm_num)5253universe v54variable {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]5556theorem 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) := by59 apply tendsto_projection_orbit_zero tracePositive trace_mul_comm σ ξ hξ60 rootFlag isStarProjection_rootFlag (fun n ↦ (2 ^ n : ℝ)⁻¹)61 · intro n62 simp only [tracePositive_apply, trace_rootFlag, Complex.ofReal_inv,63 Complex.ofReal_pow, Complex.ofReal_ofNat]64 · exact tendsto_inv_pow_two_atTop_nhds_zero6566theorem 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) := by71 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 n75 simp only [tracePositive_apply, trace_transportedFlag, Complex.ofReal_inv,76 Complex.ofReal_pow, Complex.ofReal_ofNat]77 · exact tendsto_inv_pow_two_atTop_nhds_zero7879end MathlibAnnex.CStarAlgebra.CAR