Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/CyclicCapture.lean, lines 109–207.
Back to Assembling selected GNS cyclic subspaces into an isometric source representation
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.CaptureSurviving 2import MathlibAnnex.Analysis.CStarAlgebra.Representation.CyclicRestriction 3 4/-! 5# Cyclic pieces carried by the target defect vectors 6 7Each vector supplied by the completed-CAR compression theorem generates a 8closed reducing copy of the corresponding selected pure GNS representation. 9Distinct selected classes give orthogonal cyclic pieces. 10-/ 11 12set_option autoImplicit false 13set_option maxHeartbeats 1200000 14 15noncomputable section 16 17open scoped ComplexOrder InnerProduct 18 19namespace MathlibAnnex.CStarAlgebra.CAR 20 21open MathlibAnnex.Analysis.CStarAlgebra 22open MathlibAnnex.Analysis.InnerProductSpace 23 24universe v 25 26/-- A unit vector with one of the selected vector states generates an 27irreducible cyclic restriction, unitarily equivalent to that selected GNS 28fiber. -/ 29theorem exists_selectedCyclicUnitary 30 {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] 31 [CompleteSpace K] (sigma : Representation Limit K) 32 (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) (eta : K) (heta : ‖eta‖ = 1) 33 (hstate : Representation.vectorFunctional sigma eta = 34 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState i).1) : 35 let M := Representation.cyclicSubspace sigma eta 36 letI : CompleteSpace M := 37 (Representation.isClosed_cyclicSubspace sigma eta).completeSpace_coe 38 let tau := Representation.restrictToReducing sigma M 39 (Representation.reduces_cyclicSubspace sigma eta) 40 ∃ U : MathlibAnnex.CStarAlgebra.PureState.SelectedGNS completedRootPureState i ≃ₗᵢ[ℂ] M, 41 tau.IsIrreducible ∧ 42 U (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i) = 43 (⟨eta, Representation.self_mem_cyclicSubspace sigma eta⟩ : M) ∧ 44 ∀ a, (U : MathlibAnnex.CStarAlgebra.PureState.SelectedGNS completedRootPureState i →L[ℂ] M).comp 45 (MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState i a) = 46 (tau a).comp 47 (U : MathlibAnnex.CStarAlgebra.PureState.SelectedGNS completedRootPureState i →L[ℂ] M) := by 48 dsimp only 49 letI : CompleteSpace (Representation.cyclicSubspace sigma eta) := 50 (Representation.isClosed_cyclicSubspace sigma eta).completeSpace_coe 51 let z : Representation.cyclicSubspace sigma eta := 52 ⟨eta, Representation.self_mem_cyclicSubspace sigma eta⟩ 53 let tau := Representation.restrictToReducing sigma 54 (Representation.cyclicSubspace sigma eta) 55 (Representation.reduces_cyclicSubspace sigma eta) 56 have hz : ‖z‖ = 1 := by simpa [z] using heta 57 have hzstate : Representation.vectorFunctional tau z = 58 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState i).1 := by 59 rw [Representation.vectorFunctional_restrictToReducing] 60 exact hstate 61 have hcyclic : DenseRange (StarAlgHom.orbitMap tau z) := by 62 exact Representation.denseRange_orbitMap_restrictCyclic sigma eta 63 have hpure : IsPureState Limit (Representation.vectorFunctional tau z) := by 64 rw [hzstate] 65 exact (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState i).2 66 have hstar : StarAlgHom.IsIrreducible tau := 67 MathlibAnnex.CStarAlgebra.isIrreducible_starAlgHom_of_isPureState tau z hz hcyclic hpure 68 have hz_ne : z ≠ 0 := by 69 intro hzero 70 simpa [hzero] using hz 71 letI : Nontrivial (Representation.cyclicSubspace sigma eta) := 72 nontrivial_of_ne z 0 hz_ne 73 have hirr : tau.IsIrreducible := 74 (Representation.isIrreducible_iff_starAlgHom tau).2 hstar 75 have hsourceCyclic : DenseRange (StarAlgHom.orbitMap 76 (MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState i) 77 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i)) := 78 MathlibAnnex.CStarAlgebra.PureState.denseRange_representative_gns_orbit completedRootPureState i 79 have hcoeff (a : Limit) : 80 inner ℂ (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i) 81 (MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState i a 82 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i)) = 83 inner ℂ z (tau a z) := by 84 calc 85 inner ℂ (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i) 86 (MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState i a 87 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i)) = 88 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState i).1 a := by 89 have h := congrArg (fun f : Limit →L[ℂ] ℂ ↦ f a) 90 (MathlibAnnex.CStarAlgebra.PureState.selected_vectorFunctional completedRootPureState i) 91 exact h 92 _ = Representation.vectorFunctional tau z a := by rw [hzstate] 93 _ = inner ℂ z (tau a z) := rfl 94 obtain ⟨U, hU, -⟩ := StarAlgHom.existsUnique_pointedCyclicTransport 95 (MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState i) tau 96 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i) z 97 hsourceCyclic hcyclic hcoeff 98 refine ⟨U, ?_⟩ 99 simpa [tau, z] using (show tau.IsIrreducible ∧ 100 U (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i) = z ∧ 101 ∀ a, (U : MathlibAnnex.CStarAlgebra.PureState.SelectedGNS completedRootPureState i →L[ℂ] 102 Representation.cyclicSubspace sigma eta).comp 103 (MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState i a) = 104 (tau a).comp 105 (U : MathlibAnnex.CStarAlgebra.PureState.SelectedGNS completedRootPureState i →L[ℂ] 106 Representation.cyclicSubspace sigma eta) from 107 ⟨hirr, hU.2.1, hU.2.2⟩) 108 109/-- Cyclic subspaces carrying two distinct selected pure-state classes are 110orthogonal. The projection from one cyclic piece to the other is an 111intertwiner; Schur and the chosen-representative separation force it to 112vanish. -/ 113theorem isOrtho_cyclicSubspace_of_selectedStates 114 {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] 115 [CompleteSpace K] (sigma : Representation Limit K) 116 {i j : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit} (hij : i ≠ j) 117 (eta_i eta_j : K) (heta_i : ‖eta_i‖ = 1) (heta_j : ‖eta_j‖ = 1) 118 (hstate_i : Representation.vectorFunctional sigma eta_i = 119 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState i).1) 120 (hstate_j : Representation.vectorFunctional sigma eta_j = 121 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState j).1) : 122 Representation.cyclicSubspace sigma eta_i ⟂ 123 Representation.cyclicSubspace sigma eta_j := by 124 let Mi := Representation.cyclicSubspace sigma eta_i 125 let Mj := Representation.cyclicSubspace sigma eta_j 126 have hMiClosed : IsClosed (Mi : Set K) := 127 Representation.isClosed_cyclicSubspace sigma eta_i 128 have hMjClosed : IsClosed (Mj : Set K) := 129 Representation.isClosed_cyclicSubspace sigma eta_j 130 letI : CompleteSpace Mi := hMiClosed.completeSpace_coe 131 letI : CompleteSpace Mj := hMjClosed.completeSpace_coe 132 letI : Mi.HasOrthogonalProjection := by 133 letI : IsClosed (Mi : Set K) := hMiClosed 134 infer_instance 135 let tau_i := Representation.restrictToReducing sigma Mi 136 (Representation.reduces_cyclicSubspace sigma eta_i) 137 let tau_j := Representation.restrictToReducing sigma Mj 138 (Representation.reduces_cyclicSubspace sigma eta_j) 139 obtain ⟨Ui, hirri, -, hUi⟩ := 140 exists_selectedCyclicUnitary sigma i eta_i heta_i hstate_i 141 obtain ⟨Uj, hirrj, -, hUj⟩ := 142 exists_selectedCyclicUnitary sigma j eta_j heta_j hstate_j 143 let zi : Mi := ⟨eta_i, Representation.self_mem_cyclicSubspace sigma eta_i⟩ 144 let zj : Mj := ⟨eta_j, Representation.self_mem_cyclicSubspace sigma eta_j⟩ 145 have hzi_ne : zi ≠ 0 := by 146 intro hzero 147 have h := congrArg norm hzero 148 simpa [zi, heta_i] using h 149 have hzj_ne : zj ≠ 0 := by 150 intro hzero 151 have h := congrArg norm hzero 152 simpa [zj, heta_j] using h 153 letI : Nontrivial Mi := nontrivial_of_ne zi 0 hzi_ne 154 letI : Nontrivial Mj := nontrivial_of_ne zj 0 hzj_ne 155 let V : Mj →L[ℂ] Mi := Mi.orthogonalProjectionOnto.comp Mj.subtypeL 156 have hV : StarAlgHom.Intertwines tau_j tau_i V := by 157 intro a 158 apply ContinuousLinearMap.ext 159 intro x 160 apply Subtype.ext 161 have hcomm := Representation.starProjection_commutes_of_reduces sigma Mi 162 (Representation.reduces_cyclicSubspace sigma eta_i) a 163 have hx := congrArg (fun T : K →L[ℂ] K ↦ T (x : K)) hcomm 164 change Mi.starProjection (sigma a (x : K)) = 165 sigma a (Mi.starProjection (x : K)) 166 exact hx 167 have hno (E : Mj ≃ₗᵢ[ℂ] Mi) : 168 ¬ StarAlgHom.Intertwines tau_j tau_i (E : Mj →L[ℂ] Mi) := by 169 intro hE 170 have hUjEq : Representation.UnitaryEquivalent 171 (MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState j) tau_j := by 172 refine ⟨Uj, fun a x ↦ ?_⟩ 173 have h := congrArg 174 (fun T : MathlibAnnex.CStarAlgebra.PureState.SelectedGNS completedRootPureState j →L[ℂ] Mj ↦ T x) 175 (hUj a) 176 simpa [ContinuousLinearMap.comp_apply] using h 177 have hEEq : Representation.UnitaryEquivalent tau_j tau_i := by 178 refine ⟨E, fun a x ↦ ?_⟩ 179 have h := congrArg (fun T : Mj →L[ℂ] Mi ↦ T x) (hE a) 180 simpa [ContinuousLinearMap.comp_apply] using h 181 have hUiEq : Representation.UnitaryEquivalent 182 (MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState i) tau_i := by 183 refine ⟨Ui, fun a x ↦ ?_⟩ 184 have h := congrArg 185 (fun T : MathlibAnnex.CStarAlgebra.PureState.SelectedGNS completedRootPureState i →L[ℂ] Mi ↦ T x) 186 (hUi a) 187 simpa [ContinuousLinearMap.comp_apply] using h 188 have hselected : Representation.UnitaryEquivalent 189 (MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState j) 190 (MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState i) := 191 Representation.unitaryEquivalent_trans hUjEq 192 (Representation.unitaryEquivalent_trans hEEq 193 (Representation.unitaryEquivalent_symm hUiEq)) 194 obtain ⟨W, hW⟩ := hselected 195 apply MathlibAnnex.CStarAlgebra.PureState.no_unitaryIntertwiner_selectedRepresentation 196 completedRootPureState hij.symm W 197 intro a 198 apply ContinuousLinearMap.ext 199 intro x 200 simpa [ContinuousLinearMap.comp_apply] using hW a x 201 have hVzero : V = 0 := 202 StarAlgHom.Intertwines.eq_zero_of_no_unitary 203 (Representation.isIrreducible_starAlgHom tau_j hirrj) 204 (Representation.isIrreducible_starAlgHom tau_i hirri) 205 hno hV 206 apply Submodule.orthogonalProjectionOnto_comp_subtypeL_eq_zero_iff.mp 207 simpa [V] using hVzero 208 209/-- On its own cyclic pure-state piece, the ambient common fixed projection 210has image in the distinguished one-dimensional line. This is an ambient-to- 211cyclic restriction statement, not an ambient multiplicity claim. -/ 212theorem initialFixedProjection_maps_ownCyclic 213 (family : RepresentativeShellFamily) 214 {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] 215 [CompleteSpace K] (sigma : Representation Limit K) 216 (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) (eta : K) 217 (hfixed : ∀ n, sigma (transportedFlag family i n) eta = eta) 218 {x : K} (hx : x ∈ Representation.cyclicSubspace sigma eta) : 219 commonFixedProjection (fun n ↦ sigma (transportedFlag family i n)) x ∈ 220 ℂ ∙ eta := by 221 let q := transportedFlag family i 222 let phi : Limit →L[ℂ] ℂ := 223 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState i).1 224 let P : K →L[ℂ] K := commonFixedProjection (fun n ↦ sigma (q n)) 225 have hPeta : P eta = eta := by 226 exact (commonFixedProjection_eq_self_iff (fun n ↦ sigma (q n)) eta).2 227 ((mem_commonFixedSubspace_iff (fun n ↦ sigma (q n)) eta).2 hfixed) 228 have hoperator (b : Limit) : P * sigma b * P = (phi b) • P := by 229 exact commonFixedProjection_comp_map_comp_eq sigma 230 (Representation.continuousLinearMap sigma).continuous q phi b 231 (fun n ↦ (isStarProjection_transportedFlag family i n).isSelfAdjoint.star_eq) 232 (tendsto_representative_transported_compression family i b) 233 have horbit (b : Limit) : P (sigma b eta) = phi b • eta := by 234 have h := congrArg (fun T : K →L[ℂ] K ↦ T eta) (hoperator b) 235 simpa [hPeta] using h 236 let M := Representation.cyclicSubspace sigma eta 237 letI : CompleteSpace M := 238 (Representation.isClosed_cyclicSubspace sigma eta).completeSpace_coe 239 let tau := Representation.restrictToReducing sigma M 240 (Representation.reduces_cyclicSubspace sigma eta) 241 let z : M := ⟨eta, Representation.self_mem_cyclicSubspace sigma eta⟩ 242 have hdense : DenseRange (StarAlgHom.orbitMap tau z) := 243 Representation.denseRange_orbitMap_restrictCyclic sigma eta 244 have hspanClosed : IsClosed ((ℂ ∙ eta : Submodule ℂ K) : Set K) := 245 Submodule.closed_of_finiteDimensional _ 246 have hclosed : IsClosed {y : M | P (y : K) ∈ (ℂ ∙ eta : Submodule ℂ K)} := 247 hspanClosed.preimage (P.comp M.subtypeL).continuous 248 have hall : ∀ y : M, P (y : K) ∈ (ℂ ∙ eta : Submodule ℂ K) := by 249 intro y 250 exact hdense.induction_on y hclosed fun b ↦ by 251 change P (sigma b eta) ∈ (ℂ ∙ eta : Submodule ℂ K) 252 rw [horbit b] 253 exact (ℂ ∙ eta).smul_mem (phi b) (Submodule.mem_span_singleton_self eta) 254 exact hall ⟨x, hx⟩ 255 256/-- The common fixed projection for class `i` vanishes on the cyclic piece 257of a different selected class `j`. Every nonzero vector in the ambient 258fixed range would itself carry class `i`, so orthogonality and the projection 259norm identity exclude such a component. -/ 260theorem initialFixedProjection_eq_zero_on_otherCyclic 261 (family : RepresentativeShellFamily) 262 {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] 263 [CompleteSpace K] (sigma : Representation Limit K) 264 {i j : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit} (hij : i ≠ j) 265 (eta_j : K) (heta_j : ‖eta_j‖ = 1) 266 (hstate_j : Representation.vectorFunctional sigma eta_j = 267 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState j).1) 268 {x : K} (hx : x ∈ Representation.cyclicSubspace sigma eta_j) : 269 commonFixedProjection (fun n ↦ sigma (transportedFlag family i n)) x = 0 := by 270 let q := transportedFlag family i 271 let phi : Limit →L[ℂ] ℂ := 272 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState i).1 273 let F := commonFixedSubspace (fun n ↦ sigma (q n)) 274 let P : K →L[ℂ] K := commonFixedProjection (fun n ↦ sigma (q n)) 275 let y : K := P x 276 by_contra hyzero 277 have hy_ne : y ≠ 0 := hyzero 278 let z : K := NormedSpace.normalize y 279 have hz_norm : ‖z‖ = 1 := NormedSpace.norm_normalize hy_ne 280 have hy_fixed (n : ℕ) : sigma (q n) y = y := by 281 exact commonFixedProjection_apply_fixed (fun n ↦ sigma (q n)) n x 282 have hz_fixed (n : ℕ) : sigma (q n) z = z := by 283 change sigma (q n) (((‖y‖⁻¹ : ℝ) : ℂ) • y) = 284 ((‖y‖⁻¹ : ℝ) : ℂ) • y 285 rw [map_smul, hy_fixed] 286 have hz_state : Representation.vectorFunctional sigma z = phi := by 287 apply vectorFunctional_eq_of_compression_tendsto sigma q phi 288 (fun n ↦ (isStarProjection_transportedFlag family i n).isSelfAdjoint.star_eq) 289 (tendsto_representative_transported_compression family i) 290 z hz_norm hz_fixed 291 have horth := isOrtho_cyclicSubspace_of_selectedStates sigma hij z eta_j 292 hz_norm heta_j hz_state hstate_j 293 have hzx : inner ℂ z x = 0 := horth.inner_eq 294 (Representation.self_mem_cyclicSubspace sigma z) hx 295 have hy_eq : y = (‖y‖ : ℂ) • z := by 296 simpa [z, Complex.real_smul] using (NormedSpace.norm_smul_normalize y).symm 297 have hyx : inner ℂ y x = 0 := by 298 rw [hy_eq, inner_smul_left, hzx, mul_zero] 299 have hnormsq := Submodule.re_inner_starProjection_eq_normSq F x 300 change (inner ℂ (P x) x).re = ‖P x‖ ^ 2 at hnormsq 301 have hnorm_zero : ‖y‖ ^ 2 = 0 := by 302 calc 303 ‖y‖ ^ 2 = (inner ℂ y x).re := hnormsq.symm 304 _ = 0 := by rw [hyx]; rfl 305 exact hy_ne (norm_eq_zero.mp (sq_eq_zero_iff.mp hnorm_zero)) 306 307/-- The cyclic copies of all selected pure states assemble to an isometric 308source intertwiner from the displayed arbitrary-index atomic Hilbert sum into 309the target Hilbert space. The ambient fixed projection for class `i` maps 310the isometry range into the distinguished line carried by the `i`-th selected 311vector (and hence back into the isometry range). Surjectivity is deliberately 312not asserted here; it is the remaining generated-target reduction step. -/ 313theorem exists_selectedAtomicCyclicIsometry 314 (family : RepresentativeShellFamily) 315 {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] 316 [CompleteSpace K] (sigma : Representation Limit K) 317 (eta : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit → K) 318 (heta : ∀ i, ‖eta i‖ = 1) 319 (hstate : ∀ i, Representation.vectorFunctional sigma (eta i) = 320 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState i).1) : 321 ∃ W : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →ₗᵢ[ℂ] K, 322 (∀ i x, W (MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState i x) ∈ 323 Representation.cyclicSubspace sigma (eta i)) ∧ 324 (∀ i, W (MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState i 325 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i)) = eta i) ∧ 326 (∀ i x, commonFixedProjection 327 (fun n ↦ sigma (transportedFlag family i n)) (W x) ∈ 328 ℂ ∙ eta i) ∧ 329 ∀ a, 330 W.toContinuousLinearMap.comp 331 (selectedAtomicRepresentation a) = 332 (sigma a).comp 333 W.toContinuousLinearMap := by 334 classical 335 let M (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) := 336 Representation.cyclicSubspace sigma (eta i) 337 letI instComplete (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) : CompleteSpace (M i) := 338 (Representation.isClosed_cyclicSubspace sigma (eta i)).completeSpace_coe 339 have hex (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) : 340 ∃ U : MathlibAnnex.CStarAlgebra.PureState.SelectedGNS completedRootPureState i ≃ₗᵢ[ℂ] M i, 341 let tau := Representation.restrictToReducing sigma (M i) 342 (Representation.reduces_cyclicSubspace sigma (eta i)) 343 tau.IsIrreducible ∧ 344 U (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i) = 345 (⟨eta i, Representation.self_mem_cyclicSubspace sigma (eta i)⟩ : M i) ∧ 346 ∀ a, (U : MathlibAnnex.CStarAlgebra.PureState.SelectedGNS completedRootPureState i →L[ℂ] M i).comp 347 (MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState i a) = 348 (tau a).comp 349 (U : MathlibAnnex.CStarAlgebra.PureState.SelectedGNS completedRootPureState i →L[ℂ] M i) := by 350 simpa [M] using 351 exists_selectedCyclicUnitary sigma i (eta i) (heta i) (hstate i) 352 choose U hU using hex 353 let V (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) : 354 MathlibAnnex.CStarAlgebra.PureState.SelectedGNS completedRootPureState i →ₗᵢ[ℂ] K := 355 (M i).subtypeₗᵢ.comp (U i).toLinearIsometry 356 have hVortho : OrthogonalFamily ℂ 357 (MathlibAnnex.CStarAlgebra.PureState.SelectedGNS completedRootPureState) V := by 358 intro i j hij x y 359 have horth := isOrtho_cyclicSubspace_of_selectedStates sigma hij 360 (eta i) (eta j) (heta i) (heta j) (hstate i) (hstate j) 361 exact horth.inner_eq (by 362 change (U i x : K) ∈ Representation.cyclicSubspace sigma (eta i) 363 exact (U i x).property) (by 364 change (U j y : K) ∈ Representation.cyclicSubspace sigma (eta j) 365 exact (U j y).property) 366 let W : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →ₗᵢ[ℂ] K := 367 hVortho.linearIsometry 368 have hWpoint (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) : 369 W (MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState i 370 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i)) = eta i := by 371 have hsingle := OrthogonalFamily.linearIsometry_apply_single hVortho 372 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i) 373 calc 374 W (MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState i 375 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i)) = 376 V i (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i) := by 377 simpa [W, MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding, 378 MathlibAnnex.Analysis.InnerProductSpace.coordinateEmbedding_apply] using hsingle 379 _ = eta i := by 380 have h := congrArg Subtype.val ((hU i).2.1) 381 simpa [V] using h 382 have hVintertwines (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) (a : Limit) 383 (x : MathlibAnnex.CStarAlgebra.PureState.SelectedGNS completedRootPureState i) : 384 V i (MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState i a x) = 385 sigma a (V i x) := by 386 have h := congrArg 387 (fun T : MathlibAnnex.CStarAlgebra.PureState.SelectedGNS completedRootPureState i →L[ℂ] M i ↦ T x) 388 ((hU i).2.2 a) 389 have h' := congrArg Subtype.val h 390 simpa [V, ContinuousLinearMap.comp_apply, 391 Representation.restrictToReducing_apply_coe] using h' 392 refine ⟨W, ?_, ?_, ?_, ?_⟩ 393 · intro i x 394 have hsingle := OrthogonalFamily.linearIsometry_apply_single hVortho x 395 have heq : W (MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState i x) = 396 V i x := by 397 simpa [W, MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding, 398 MathlibAnnex.Analysis.InnerProductSpace.coordinateEmbedding_apply] using hsingle 399 rw [heq] 400 change (U i x : K) ∈ Representation.cyclicSubspace sigma (eta i) 401 exact (U i x).property 402 · intro i 403 exact hWpoint i 404 · intro i x 405 let P : K →L[ℂ] K := commonFixedProjection 406 (fun n ↦ sigma (transportedFlag family i n)) 407 have hsum : Summable (fun j ↦ V j (x j)) := hVortho.summable_of_lp x 408 have hother (j : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) (hji : j ≠ i) : 409 P (V j (x j)) = 0 := by 410 apply initialFixedProjection_eq_zero_on_otherCyclic family sigma hji.symm 411 (eta j) (heta j) (hstate j) 412 change (U j (x j) : K) ∈ Representation.cyclicSubspace sigma (eta j) 413 exact (U j (x j)).property 414 have hcollapse : (∑' j, P (V j (x j))) = P (V i (x i)) := by 415 exact tsum_eq_single i hother 416 have hfixed_i (n : ℕ) : 417 sigma (transportedFlag family i n) (eta i) = eta i := by 418 apply projection_apply_eq_self_of_vectorFunctional_eq_one sigma 419 (transportedFlag family i n) (isStarProjection_transportedFlag family i n) 420 (eta i) (heta i) 421 rw [hstate i] 422 calc 423 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState i).1 424 (transportedFlag family i n) = rootState (rootFlag n) := 425 (representativeShellData family i).state_eq (rootFlag n) 426 _ = 1 := rootState_rootFlag n 427 have hown : P (V i (x i)) ∈ (ℂ ∙ eta i : Submodule ℂ K) := by 428 apply initialFixedProjection_maps_ownCyclic family sigma i (eta i) 429 hfixed_i 430 change (U i (x i) : K) ∈ Representation.cyclicSubspace sigma (eta i) 431 exact (U i (x i)).property 432 have hPW : P (W x) = P (V i (x i)) := by 433 calc 434 P (W x) = P (∑' j, V j (x j)) := by 435 rw [OrthogonalFamily.linearIsometry_apply hVortho] 436 _ = ∑' j, P (V j (x j)) := P.map_tsum hsum 437 _ = P (V i (x i)) := hcollapse 438 rw [hPW] 439 exact hown 440 · intro a 441 apply ContinuousLinearMap.ext 442 intro x 443 change W (selectedAtomicRepresentation a x) = sigma a (W x) 444 calc 445 W (selectedAtomicRepresentation a x) = 446 ∑' i, V i ((selectedAtomicRepresentation a x) i) := by 447 exact OrthogonalFamily.linearIsometry_apply hVortho _ 448 _ = ∑' i, V i 449 (MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState i a (x i)) := by 450 apply tsum_congr 451 intro i 452 rw [selectedAtomicRepresentation] 453 rfl 454 _ = ∑' i, sigma a (V i (x i)) := by 455 apply tsum_congr 456 intro i 457 exact hVintertwines i a (x i) 458 _ = sigma a (∑' i, V i (x i)) := by 459 exact ((sigma a).map_tsum (hVortho.summable_of_lp x)).symm 460 _ = sigma a (W x) := by 461 rw [OrthogonalFamily.linearIsometry_apply hVortho] 462 463end MathlibAnnex.CStarAlgebra.CAR