Exact source: MathlibAnnex/Analysis/CStarAlgebra/GNS/TracialProjection.lean, lines 85–95.
Back to Transported flags vanish on vectors generated by a trace vector
1import MathlibAnnex.Analysis.CStarAlgebra.Representation.Cyclic 2import MathlibAnnex.Analysis.CStarAlgebra.Representation.VectorFunctional 3import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order 4import Mathlib.Analysis.SpecificLimits.Basic 5 6/-! 7# Vanishing projection flags in a tracial cyclic subspace 8 9A trace estimate is first established on every source-orbit vector. The 10limiting projection is then shown to vanish on the closed source-cyclic 11subspace. The ambient representation need not be tracial or cyclic. 12-/ 13 14set_option autoImplicit false 15 16open Filter Topology 17open scoped ComplexOrder InnerProduct 18 19namespace MathlibAnnex.Analysis.CStarAlgebra 20 21universe u v 22 23variable {A : Type u} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] 24variable {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] 25 26/-- Cyclicity is not needed for the projection estimate; agreement of the 27vector 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 := by 34 have hsquare : star (p * b) * (p * b) = star b * p * b := by 35 calc 36 star (p * b) * (p * b) = (star b * p) * (p * b) := by 37 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 _ _ _).symm 41 have hnorm : τ (star b * p * b) = ((‖σ p (σ b ξ)‖ ^ 2 : ℝ) : ℂ) := by 42 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_cast 46 have hcyclic : τ (star b * p * b) = τ (p * (b * star b) * p) := by 47 calc 48 τ (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 := by 54 have h := CStarAlgebra.star_left_conjugate_le_norm_smul 55 (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 h 58 have hbound := OrderHomClass.mono τ horder 59 have hscalar : τ (‖b‖ ^ 2 • p) = ((‖b‖ ^ 2 * r : ℝ) : ℂ) := by 60 rw [← Complex.coe_smul, map_smul, hr] 61 simp only [smul_eq_mul, Complex.ofReal_mul] 62 rw [← hcyclic, hnorm, hscalar] at hbound 63 have hre := (RCLike.nonneg_iff.mp (sub_nonneg.mpr hbound)).1 64 change 0 ≤ Complex.re 65 (((‖b‖ ^ 2 * r : ℝ) : ℂ) - ((‖σ p (σ b ξ)‖ ^ 2 : ℝ) : ℂ)) at hre 66 simpa only [Complex.sub_re, Complex.ofReal_re, sub_nonneg] using hre 67 68/-- 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) := by 73 have hsquare : Tendsto (fun n ↦ ‖x n‖ ^ 2) atTop (nhds 0) := 74 squeeze_zero (fun n ↦ sq_nonneg _) hbound 75 (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.mp 79 ((tendsto_order.mp hsquare).2 (ε ^ 2) (sq_pos_of_pos hε)) 80 refine ⟨N, fun n hn ↦ ?_⟩ 81 have h := hN n hn 82 rw [dist_zero_right] 83 nlinarith [norm_nonneg (x n)] 84 85theorem 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) r 94 (fun n ↦ norm_sq_projection_orbit_le τ hτ σ ξ hξ (p n) (hp n) (r n) 95 (hvalue n) b) hr 96 97/-- A projection onto the common range is fixed by every projection in the 98flag. This is a finite operator identity, not a continuity assertion. -/ 99theorem projection_mul_eq_self_of_range_eq_iInf 100 (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 := by 104 have hleft : Q n * P = P := by 105 apply ContinuousLinearMap.ext 106 intro x 107 have hx : P x ∈ (Q n).range := by 108 have hmem : P x ∈ P.range := ⟨x, rfl⟩ 109 rw [hrange] at hmem 110 exact (Submodule.mem_iInf (fun n ↦ (Q n).range)).mp hmem n 111 obtain ⟨y, hy⟩ := hx 112 change Q n (P x) = P x 113 rw [← hy] 114 exact congrArg (fun T : H →L[ℂ] H ↦ T y) (hQ n).isIdempotentElem.eq 115 refine ⟨hleft, ?_⟩ 116 have h := congrArg star hleft 117 simpa only [star_mul, hP.isSelfAdjoint.star_eq, (hQ n).isSelfAdjoint.star_eq] using h 118 119/-- The common-range projection kills the whole closed source-cyclic 120subspace once the flag tends to zero on each source-orbit vector. -/ 121theorem projection_eq_zero_on_cyclicSubspace 122 (σ : 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 := by 128 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).2 131 have horbit (b : A) : P (σ b ξ) = 0 := by 132 have hlim : Tendsto (fun n ↦ P (σ (p n) (σ b ξ))) atTop (nhds 0) := by 133 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 ξ) := by 136 funext n 137 change (P * σ (p n)) (σ b ξ) = P (σ b ξ) 138 rw [hPe n] 139 rw [heq] at hlim 140 exact tendsto_nhds_unique tendsto_const_nhds hlim 141 have hclosed : IsClosed {x : H | P x = 0} := 142 isClosed_eq P.continuous continuous_const 143 intro x hx 144 have hx' : x ∈ closure (Set.range (Representation.orbitLinearMap σ ξ)) := by 145 change x ∈ (Representation.cyclicSubspace σ ξ : Set H) at hx 146 simpa only [Representation.cyclicSubspace, Submodule.topologicalClosure_coe, 147 LinearMap.coe_range] using hx 148 apply closure_minimal (t := {x : H | P x = 0}) _ hclosed hx' 149 rintro _ ⟨b, rfl⟩ 150 exact horbit b 151 152end MathlibAnnex.Analysis.CStarAlgebra