Exact source: MathlibAnnex/Analysis/CStarAlgebra/GNS/TracialProjection.lean
Pinned GitHub source · Raw UTF-8 source
Back to Transported flags vanish on vectors generated by a trace vector
1import MathlibAnnex.Analysis.CStarAlgebra.Representation.Cyclic2import MathlibAnnex.Analysis.CStarAlgebra.Representation.VectorFunctional3import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order4import Mathlib.Analysis.SpecificLimits.Basic56/-!7# Vanishing projection flags in a tracial cyclic subspace89A trace estimate is first established on every source-orbit vector. The10limiting projection is then shown to vanish on the closed source-cyclic11subspace. The ambient representation need not be tracial or cyclic.12-/1314set_option autoImplicit false1516open Filter Topology17open scoped ComplexOrder InnerProduct1819namespace MathlibAnnex.Analysis.CStarAlgebra2021universe u v2223variable {A : Type u} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]24variable {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]2526/-- Cyclicity is not needed for the projection estimate; agreement of the27vector functional with the tracial positive functional suffices. -/28theorem norm_sq_projection_orbit_le (τ : A →ₚ[ℂ] ℂ)29 (hτ : ∀ a b, τ (a * b) = τ (b * a))30 (σ : Representation A H) (ξ : H)31 (hξ : ∀ a, Representation.vectorFunctional σ ξ a = τ a)32 (p : A) (hp : IsStarProjection p) (r : ℝ) (hr : τ p = (r : ℂ))33 (b : A) : ‖σ p (σ b ξ)‖ ^ 2 ≤ ‖b‖ ^ 2 * r := by34 have hsquare : star (p * b) * (p * b) = star b * p * b := by35 calc36 star (p * b) * (p * b) = (star b * p) * (p * b) := by37 rw [star_mul, hp.isSelfAdjoint.star_eq]38 _ = star b * ((p * p) * b) := by simp only [mul_assoc]39 _ = star b * (p * b) := by rw [hp.isIdempotentElem.eq]40 _ = star b * p * b := (mul_assoc _ _ _).symm41 have hnorm : τ (star b * p * b) = ((‖σ p (σ b ξ)‖ ^ 2 : ℝ) : ℂ) := by42 rw [← hsquare, ← hξ, Representation.vectorFunctional_star_mul,43 inner_self_eq_norm_sq_to_K, map_mul]44 simp only [mul_apply_eq_comp]45 norm_cast46 have hcyclic : τ (star b * p * b) = τ (p * (b * star b) * p) := by47 calc48 τ (star b * p * b) = τ (star b * (p * b)) := by rw [mul_assoc]49 _ = τ (star b * ((p * p) * b)) := by rw [hp.isIdempotentElem.eq]50 _ = τ ((star b * p) * (p * b)) := by simp only [mul_assoc]51 _ = τ ((p * b) * (star b * p)) := hτ _ _52 _ = τ (p * (b * star b) * p) := by simp only [mul_assoc]53 have horder : p * (b * star b) * p ≤ ‖b‖ ^ 2 • p := by54 have h := CStarAlgebra.star_left_conjugate_le_norm_smul55 (a := p) (b := b * star b) (IsSelfAdjoint.mul_star_self b)56 simpa only [hp.isSelfAdjoint.star_eq, hp.isIdempotentElem.eq,57 CStarRing.norm_self_mul_star, sq] using h58 have hbound := OrderHomClass.mono τ horder59 have hscalar : τ (‖b‖ ^ 2 • p) = ((‖b‖ ^ 2 * r : ℝ) : ℂ) := by60 rw [← Complex.coe_smul, map_smul, hr]61 simp only [smul_eq_mul, Complex.ofReal_mul]62 rw [← hcyclic, hnorm, hscalar] at hbound63 have hre := (RCLike.nonneg_iff.mp (sub_nonneg.mpr hbound)).164 change 0 ≤ Complex.re65 (((‖b‖ ^ 2 * r : ℝ) : ℂ) - ((‖σ p (σ b ξ)‖ ^ 2 : ℝ) : ℂ)) at hre66 simpa only [Complex.sub_re, Complex.ofReal_re, sub_nonneg] using hre6768/-- A square-norm bound tending to zero gives vectorwise convergence. -/69theorem tendsto_zero_of_norm_sq_le {E : Type*} [SeminormedAddCommGroup E]70 (x : ℕ → E) (c : ℝ) (r : ℕ → ℝ)71 (hbound : ∀ n, ‖x n‖ ^ 2 ≤ c * r n)72 (hr : Tendsto r atTop (nhds 0)) : Tendsto x atTop (nhds 0) := by73 have hsquare : Tendsto (fun n ↦ ‖x n‖ ^ 2) atTop (nhds 0) :=74 squeeze_zero (fun n ↦ sq_nonneg _) hbound75 (by simpa only [mul_zero] using tendsto_const_nhds.mul hr)76 rw [Metric.tendsto_atTop]77 intro ε hε78 obtain ⟨N, hN⟩ := eventually_atTop.mp79 ((tendsto_order.mp hsquare).2 (ε ^ 2) (sq_pos_of_pos hε))80 refine ⟨N, fun n hn ↦ ?_⟩81 have h := hN n hn82 rw [dist_zero_right]83 nlinarith [norm_nonneg (x n)]8485theorem tendsto_projection_orbit_zero (τ : A →ₚ[ℂ] ℂ)86 (hτ : ∀ a b, τ (a * b) = τ (b * a))87 (σ : Representation A H) (ξ : H)88 (hξ : ∀ a, Representation.vectorFunctional σ ξ a = τ a)89 (p : ℕ → A) (hp : ∀ n, IsStarProjection (p n))90 (r : ℕ → ℝ) (hvalue : ∀ n, τ (p n) = (r n : ℂ))91 (hr : Tendsto r atTop (nhds 0)) (b : A) :92 Tendsto (fun n ↦ σ (p n) (σ b ξ)) atTop (nhds 0) :=93 tendsto_zero_of_norm_sq_le _ (‖b‖ ^ 2) r94 (fun n ↦ norm_sq_projection_orbit_le τ hτ σ ξ hξ (p n) (hp n) (r n)95 (hvalue n) b) hr9697/-- A projection onto the common range is fixed by every projection in the98flag. This is a finite operator identity, not a continuity assertion. -/99theorem projection_mul_eq_self_of_range_eq_iInf100 (Q : ℕ → H →L[ℂ] H) (hQ : ∀ n, IsStarProjection (Q n))101 (P : H →L[ℂ] H) (hP : IsStarProjection P)102 (hrange : P.range = ⨅ n, (Q n).range) (n : ℕ) :103 Q n * P = P ∧ P * Q n = P := by104 have hleft : Q n * P = P := by105 apply ContinuousLinearMap.ext106 intro x107 have hx : P x ∈ (Q n).range := by108 have hmem : P x ∈ P.range := ⟨x, rfl⟩109 rw [hrange] at hmem110 exact (Submodule.mem_iInf (fun n ↦ (Q n).range)).mp hmem n111 obtain ⟨y, hy⟩ := hx112 change Q n (P x) = P x113 rw [← hy]114 exact congrArg (fun T : H →L[ℂ] H ↦ T y) (hQ n).isIdempotentElem.eq115 refine ⟨hleft, ?_⟩116 have h := congrArg star hleft117 simpa only [star_mul, hP.isSelfAdjoint.star_eq, (hQ n).isSelfAdjoint.star_eq] using h118119/-- The common-range projection kills the whole closed source-cyclic120subspace once the flag tends to zero on each source-orbit vector. -/121theorem projection_eq_zero_on_cyclicSubspace122 (σ : Representation A H) (ξ : H) (p : ℕ → A)123 (hp : ∀ n, IsStarProjection (p n))124 (hzero : ∀ b, Tendsto (fun n ↦ σ (p n) (σ b ξ)) atTop (nhds 0))125 (P : H →L[ℂ] H) (hP : IsStarProjection P)126 (hrange : P.range = ⨅ n, (σ (p n)).range) :127 ∀ x ∈ Representation.cyclicSubspace σ ξ, P x = 0 := by128 have hPe (n : ℕ) : P * σ (p n) = P :=129 (projection_mul_eq_self_of_range_eq_iInf (fun n ↦ σ (p n))130 (fun n ↦ (hp n).map σ) P hP hrange n).2131 have horbit (b : A) : P (σ b ξ) = 0 := by132 have hlim : Tendsto (fun n ↦ P (σ (p n) (σ b ξ))) atTop (nhds 0) := by133 change Tendsto (P ∘ fun n ↦ σ (p n) (σ b ξ)) atTop (nhds 0)134 simpa only [map_zero] using (P.continuous.tendsto 0).comp (hzero b)135 have heq : (fun n ↦ P (σ (p n) (σ b ξ))) = fun _n : ℕ ↦ P (σ b ξ) := by136 funext n137 change (P * σ (p n)) (σ b ξ) = P (σ b ξ)138 rw [hPe n]139 rw [heq] at hlim140 exact tendsto_nhds_unique tendsto_const_nhds hlim141 have hclosed : IsClosed {x : H | P x = 0} :=142 isClosed_eq P.continuous continuous_const143 intro x hx144 have hx' : x ∈ closure (Set.range (Representation.orbitLinearMap σ ξ)) := by145 change x ∈ (Representation.cyclicSubspace σ ξ : Set H) at hx146 simpa only [Representation.cyclicSubspace, Submodule.topologicalClosure_coe,147 LinearMap.coe_range] using hx148 apply closure_minimal (t := {x : H | P x = 0}) _ hclosed hx'149 rintro _ ⟨b, rfl⟩150 exact horbit b151152end MathlibAnnex.Analysis.CStarAlgebra