Exact source: MathlibAnnex/Analysis/CStarAlgebra/Compression.lean, lines 152–172.
Back to The matching GNS fiber retains exactly its cyclic line
1import Mathlib.Analysis.InnerProductSpace.Adjoint 2import MathlibAnnex.Analysis.InnerProductSpace.CommonFixed 3 4/-! 5Compression of a norm-convergent source flag inside a continuous Hilbert-space 6representation. The conclusion is a matrix-coefficient identity on the common 7fixed space; no bidual or transport of strong limits through representations is 8used. 9-/ 10 11set_option autoImplicit false 12 13open Filter 14 15namespace MathlibAnnex.Analysis.CStarAlgebra 16 17variable {A H : Type*} 18variable [NormedRing A] [NormedAlgebra ℂ A] [StarRing A] 19variable [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] 20 21/-- 22If a compression error tends to zero in the source norm, then its matrix 23coefficient vanishes on vectors fixed by every member of the flag. Continuity 24of the representation is explicit; C*-representations supply it by standard 25contractivity. 26-/ 27theorem inner_map_eq_of_compression_tendsto 28 (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (hpi : Continuous pi) 29 (q : ℕ → A) (phi : A →ₗ[ℂ] ℂ) (b : A) (x y : H) 30 (hq_star : ∀ n, star (q n) = q n) 31 (hx : ∀ n, pi (q n) x = x) (hy : ∀ n, pi (q n) y = y) 32 (hcompression : 33 Tendsto (fun n ↦ q n * b * q n - (phi b) • q n) atTop (nhds 0)) : 34 inner ℂ x (pi b y) = phi b * inner ℂ x y := by 35 have hop : 36 Tendsto (fun n ↦ pi (q n * b * q n - (phi b) • q n)) atTop (nhds 0) := by 37 change Tendsto (pi ∘ fun n ↦ q n * b * q n - (phi b) • q n) atTop (nhds 0) 38 simpa only [map_zero] using (hpi.tendsto 0).comp hcompression 39 have happ : 40 Tendsto (fun n ↦ pi (q n * b * q n - (phi b) • q n) y) atTop (nhds 0) := by 41 simpa [Function.comp_def] using 42 ((ContinuousLinearMap.apply ℂ H y).continuous.tendsto 0).comp hop 43 have hinner : 44 Tendsto 45 (fun n ↦ inner ℂ x (pi (q n * b * q n - (phi b) • q n) y)) 46 atTop (nhds 0) := by 47 simpa using tendsto_const_nhds.inner happ 48 have hcoeff (n : ℕ) : 49 inner ℂ x (pi (q n * b * q n - (phi b) • q n) y) = 50 inner ℂ x (pi b y) - phi b * inner ℂ x y := by 51 have hself : ContinuousLinearMap.adjoint (pi (q n)) = pi (q n) := by 52 calc 53 ContinuousLinearMap.adjoint (pi (q n)) = star (pi (q n)) := by 54 rw [ContinuousLinearMap.star_eq_adjoint] 55 _ = pi (star (q n)) := (map_star pi (q n)).symm 56 _ = pi (q n) := by rw [hq_star n] 57 calc 58 inner ℂ x (pi (q n * b * q n - (phi b) • q n) y) = 59 inner ℂ x (pi (q n) (pi b (pi (q n) y))) - 60 inner ℂ x ((phi b) • pi (q n) y) := by 61 simp only [map_sub, map_mul, map_smul, ContinuousLinearMap.sub_apply, 62 ContinuousLinearMap.mul_apply, ContinuousLinearMap.smul_apply, inner_sub_right] 63 _ = inner ℂ x (pi (q n) (pi b y)) - 64 inner ℂ x ((phi b) • y) := by rw [hy n] 65 _ = inner ℂ (pi (q n) x) (pi b y) - 66 inner ℂ x ((phi b) • y) := by 67 simpa [hself] using 68 (ContinuousLinearMap.adjoint_inner_right (pi (q n)) x (pi b y)) 69 _ = inner ℂ x (pi b y) - phi b * inner ℂ x y := by 70 rw [hx n, inner_smul_right] 71 have hconstant : 72 Tendsto 73 (fun _ : ℕ ↦ inner ℂ x (pi b y) - phi b * inner ℂ x y) 74 atTop (nhds 0) := 75 hinner.congr' (Filter.Eventually.of_forall fun n ↦ hcoeff n) 76 have hconst : 77 Tendsto 78 (fun _ : ℕ ↦ inner ℂ x (pi b y) - phi b * inner ℂ x y) 79 atTop (nhds (inner ℂ x (pi b y) - phi b * inner ℂ x y)) := 80 tendsto_const_nhds 81 have hz : inner ℂ x (pi b y) - phi b * inner ℂ x y = 0 := 82 tendsto_nhds_unique hconst hconstant 83 exact sub_eq_zero.mp hz 84 85/-- 86Operator form of compression onto a supplied orthogonal projection whose range 87is contained in the common fixed space. This is the manuscript's compression 88formula, still without moving a strong limit through `pi`. 89-/ 90theorem projection_comp_map_comp_projection_eq 91 (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (hpi : Continuous pi) 92 (q : ℕ → A) (phi : A →ₗ[ℂ] ℂ) (b : A) 93 (hq_star : ∀ n, star (q n) = q n) 94 (hcompression : 95 Tendsto (fun n ↦ q n * b * q n - (phi b) • q n) atTop (nhds 0)) 96 (P : H →L[ℂ] H) (hP_star : ContinuousLinearMap.adjoint P = P) 97 (hP_idem : P * P = P) 98 (hP_fixed : ∀ (n : ℕ) (z : H), pi (q n) (P z) = P z) : 99 P * pi b * P = (phi b) • P := by 100 apply ContinuousLinearMap.ext 101 intro z 102 apply ext_inner_left ℂ 103 intro w 104 have hcoeff := inner_map_eq_of_compression_tendsto pi hpi q phi b (P w) (P z) 105 hq_star (fun n ↦ hP_fixed n w) (fun n ↦ hP_fixed n z) hcompression 106 have hPPinner : inner ℂ (P w) (P z) = inner ℂ w (P z) := by 107 have hPP : P (P z) = P z := by 108 have := congrArg (fun T : H →L[ℂ] H ↦ T z) hP_idem 109 simpa using this 110 calc 111 inner ℂ (P w) (P z) = 112 inner ℂ w (ContinuousLinearMap.adjoint P (P z)) := by 113 symm 114 exact ContinuousLinearMap.adjoint_inner_right P w (P z) 115 _ = inner ℂ w (P z) := by rw [hP_star, hPP] 116 calc 117 inner ℂ w ((P * pi b * P) z) = inner ℂ w (P (pi b (P z))) := rfl 118 _ = inner ℂ (P w) (pi b (P z)) := by 119 simpa [hP_star] using 120 (ContinuousLinearMap.adjoint_inner_right P w (pi b (P z))) 121 _ = phi b * inner ℂ (P w) (P z) := hcoeff 122 _ = phi b * inner ℂ w (P z) := congrArg (fun c : ℂ ↦ phi b * c) hPPinner 123 _ = inner ℂ w (((phi b) • P) z) := by 124 simp [inner_smul_right] 125 126/-- 127Compression formula for the actual orthogonal projection onto the common fixed 128space of the represented flag. 129-/ 130theorem commonFixedProjection_comp_map_comp_eq 131 (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (hpi : Continuous pi) 132 (q : ℕ → A) (phi : A →ₗ[ℂ] ℂ) (b : A) 133 (hq_star : ∀ n, star (q n) = q n) 134 (hcompression : 135 Tendsto (fun n ↦ q n * b * q n - (phi b) • q n) atTop (nhds 0)) : 136 let P := MathlibAnnex.Analysis.InnerProductSpace.commonFixedProjection 137 (fun n ↦ pi (q n)) 138 P * pi b * P = (phi b) • P := by 139 let Q : ℕ → H →L[ℂ] H := fun n ↦ pi (q n) 140 let P := MathlibAnnex.Analysis.InnerProductSpace.commonFixedProjection Q 141 exact projection_comp_map_comp_projection_eq pi hpi q phi b hq_star hcompression P 142 (MathlibAnnex.Analysis.InnerProductSpace.adjoint_commonFixedProjection Q) 143 (MathlibAnnex.Analysis.InnerProductSpace.commonFixedProjection_idempotent Q) 144 (fun n z ↦ MathlibAnnex.Analysis.InnerProductSpace.commonFixedProjection_apply_fixed Q n z) 145 146/-- 147A compression projection is rank one when the chosen vector is cyclic for the 148whole representation. The density hypothesis is essential: without it this 149does not identify an ambient common-fixed projection of arbitrary 150multiplicity. 151-/ 152theorem projection_eq_rankOne_of_dense_orbit 153 (pi : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (phi : A →ₗ[ℂ] ℂ) 154 (P : H →L[ℂ] H) (eta : H) 155 (hPeta : P eta = eta) 156 (hcompression : ∀ b : A, P * pi b * P = (phi b) • P) 157 (hphi : ∀ b : A, phi b = inner ℂ eta (pi b eta)) 158 (hdense : DenseRange (fun b : A ↦ pi b eta)) : 159 P = InnerProductSpace.rankOne ℂ eta eta := by 160 apply ContinuousLinearMap.ext 161 intro x 162 induction x using hdense.induction_on with 163 | hp => apply isClosed_eq <;> fun_prop 164 | ih b => 165 have happ := congrArg (fun T : H →L[ℂ] H ↦ T eta) (hcompression b) 166 have hPb : P (pi b eta) = phi b • eta := by 167 simpa [hPeta] using happ 168 calc 169 P (pi b eta) = phi b • eta := hPb 170 _ = inner ℂ eta (pi b eta) • eta := by rw [hphi b] 171 _ = InnerProductSpace.rankOne ℂ eta eta (pi b eta) := by 172 rw [InnerProductSpace.rankOne_apply] 173 174end MathlibAnnex.Analysis.CStarAlgebra