Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/CyclicCapture.lean
Pinned GitHub source · Raw UTF-8 source
Back to Assembling selected GNS cyclic subspaces into an isometric source representation · Back to The cyclic sum fills every irreducible target representation
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.CaptureSurviving2import MathlibAnnex.Analysis.CStarAlgebra.Representation.CyclicRestriction34/-!5# Cyclic pieces carried by the target defect vectors67Each vector supplied by the completed-CAR compression theorem generates a8closed reducing copy of the corresponding selected pure GNS representation.9Distinct selected classes give orthogonal cyclic pieces.10-/1112set_option autoImplicit false13set_option maxHeartbeats 12000001415noncomputable section1617open scoped ComplexOrder InnerProduct1819namespace MathlibAnnex.CStarAlgebra.CAR2021open MathlibAnnex.Analysis.CStarAlgebra22open MathlibAnnex.Analysis.InnerProductSpace2324universe v2526/-- A unit vector with one of the selected vector states generates an27irreducible cyclic restriction, unitarily equivalent to that selected GNS28fiber. -/29theorem exists_selectedCyclicUnitary30 {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 eta36 letI : CompleteSpace M :=37 (Representation.isClosed_cyclicSubspace sigma eta).completeSpace_coe38 let tau := Representation.restrictToReducing sigma M39 (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).comp45 (MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState i a) =46 (tau a).comp47 (U : MathlibAnnex.CStarAlgebra.PureState.SelectedGNS completedRootPureState i →L[ℂ] M) := by48 dsimp only49 letI : CompleteSpace (Representation.cyclicSubspace sigma eta) :=50 (Representation.isClosed_cyclicSubspace sigma eta).completeSpace_coe51 let z : Representation.cyclicSubspace sigma eta :=52 ⟨eta, Representation.self_mem_cyclicSubspace sigma eta⟩53 let tau := Representation.restrictToReducing sigma54 (Representation.cyclicSubspace sigma eta)55 (Representation.reduces_cyclicSubspace sigma eta)56 have hz : ‖z‖ = 1 := by simpa [z] using heta57 have hzstate : Representation.vectorFunctional tau z =58 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState i).1 := by59 rw [Representation.vectorFunctional_restrictToReducing]60 exact hstate61 have hcyclic : DenseRange (StarAlgHom.orbitMap tau z) := by62 exact Representation.denseRange_orbitMap_restrictCyclic sigma eta63 have hpure : IsPureState Limit (Representation.vectorFunctional tau z) := by64 rw [hzstate]65 exact (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState i).266 have hstar : StarAlgHom.IsIrreducible tau :=67 MathlibAnnex.CStarAlgebra.isIrreducible_starAlgHom_of_isPureState tau z hz hcyclic hpure68 have hz_ne : z ≠ 0 := by69 intro hzero70 simpa [hzero] using hz71 letI : Nontrivial (Representation.cyclicSubspace sigma eta) :=72 nontrivial_of_ne z 0 hz_ne73 have hirr : tau.IsIrreducible :=74 (Representation.isIrreducible_iff_starAlgHom tau).2 hstar75 have hsourceCyclic : DenseRange (StarAlgHom.orbitMap76 (MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState i)77 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i)) :=78 MathlibAnnex.CStarAlgebra.PureState.denseRange_representative_gns_orbit completedRootPureState i79 have hcoeff (a : Limit) :80 inner ℂ (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i)81 (MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState i a82 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i)) =83 inner ℂ z (tau a z) := by84 calc85 inner ℂ (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i)86 (MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState i a87 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i)) =88 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState i).1 a := by89 have h := congrArg (fun f : Limit →L[ℂ] ℂ ↦ f a)90 (MathlibAnnex.CStarAlgebra.PureState.selected_vectorFunctional completedRootPureState i)91 exact h92 _ = Representation.vectorFunctional tau z a := by rw [hzstate]93 _ = inner ℂ z (tau a z) := rfl94 obtain ⟨U, hU, -⟩ := StarAlgHom.existsUnique_pointedCyclicTransport95 (MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState i) tau96 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i) z97 hsourceCyclic hcyclic hcoeff98 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).comp103 (MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState i a) =104 (tau a).comp105 (U : MathlibAnnex.CStarAlgebra.PureState.SelectedGNS completedRootPureState i →L[ℂ]106 Representation.cyclicSubspace sigma eta) from107 ⟨hirr, hU.2.1, hU.2.2⟩)108109/-- Cyclic subspaces carrying two distinct selected pure-state classes are110orthogonal. The projection from one cyclic piece to the other is an111intertwiner; Schur and the chosen-representative separation force it to112vanish. -/113theorem isOrtho_cyclicSubspace_of_selectedStates114 {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 := by124 let Mi := Representation.cyclicSubspace sigma eta_i125 let Mj := Representation.cyclicSubspace sigma eta_j126 have hMiClosed : IsClosed (Mi : Set K) :=127 Representation.isClosed_cyclicSubspace sigma eta_i128 have hMjClosed : IsClosed (Mj : Set K) :=129 Representation.isClosed_cyclicSubspace sigma eta_j130 letI : CompleteSpace Mi := hMiClosed.completeSpace_coe131 letI : CompleteSpace Mj := hMjClosed.completeSpace_coe132 letI : Mi.HasOrthogonalProjection := by133 letI : IsClosed (Mi : Set K) := hMiClosed134 infer_instance135 let tau_i := Representation.restrictToReducing sigma Mi136 (Representation.reduces_cyclicSubspace sigma eta_i)137 let tau_j := Representation.restrictToReducing sigma Mj138 (Representation.reduces_cyclicSubspace sigma eta_j)139 obtain ⟨Ui, hirri, -, hUi⟩ :=140 exists_selectedCyclicUnitary sigma i eta_i heta_i hstate_i141 obtain ⟨Uj, hirrj, -, hUj⟩ :=142 exists_selectedCyclicUnitary sigma j eta_j heta_j hstate_j143 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 := by146 intro hzero147 have h := congrArg norm hzero148 simpa [zi, heta_i] using h149 have hzj_ne : zj ≠ 0 := by150 intro hzero151 have h := congrArg norm hzero152 simpa [zj, heta_j] using h153 letI : Nontrivial Mi := nontrivial_of_ne zi 0 hzi_ne154 letI : Nontrivial Mj := nontrivial_of_ne zj 0 hzj_ne155 let V : Mj →L[ℂ] Mi := Mi.orthogonalProjectionOnto.comp Mj.subtypeL156 have hV : StarAlgHom.Intertwines tau_j tau_i V := by157 intro a158 apply ContinuousLinearMap.ext159 intro x160 apply Subtype.ext161 have hcomm := Representation.starProjection_commutes_of_reduces sigma Mi162 (Representation.reduces_cyclicSubspace sigma eta_i) a163 have hx := congrArg (fun T : K →L[ℂ] K ↦ T (x : K)) hcomm164 change Mi.starProjection (sigma a (x : K)) =165 sigma a (Mi.starProjection (x : K))166 exact hx167 have hno (E : Mj ≃ₗᵢ[ℂ] Mi) :168 ¬ StarAlgHom.Intertwines tau_j tau_i (E : Mj →L[ℂ] Mi) := by169 intro hE170 have hUjEq : Representation.UnitaryEquivalent171 (MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState j) tau_j := by172 refine ⟨Uj, fun a x ↦ ?_⟩173 have h := congrArg174 (fun T : MathlibAnnex.CStarAlgebra.PureState.SelectedGNS completedRootPureState j →L[ℂ] Mj ↦ T x)175 (hUj a)176 simpa [ContinuousLinearMap.comp_apply] using h177 have hEEq : Representation.UnitaryEquivalent tau_j tau_i := by178 refine ⟨E, fun a x ↦ ?_⟩179 have h := congrArg (fun T : Mj →L[ℂ] Mi ↦ T x) (hE a)180 simpa [ContinuousLinearMap.comp_apply] using h181 have hUiEq : Representation.UnitaryEquivalent182 (MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState i) tau_i := by183 refine ⟨Ui, fun a x ↦ ?_⟩184 have h := congrArg185 (fun T : MathlibAnnex.CStarAlgebra.PureState.SelectedGNS completedRootPureState i →L[ℂ] Mi ↦ T x)186 (hUi a)187 simpa [ContinuousLinearMap.comp_apply] using h188 have hselected : Representation.UnitaryEquivalent189 (MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState j)190 (MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState i) :=191 Representation.unitaryEquivalent_trans hUjEq192 (Representation.unitaryEquivalent_trans hEEq193 (Representation.unitaryEquivalent_symm hUiEq))194 obtain ⟨W, hW⟩ := hselected195 apply MathlibAnnex.CStarAlgebra.PureState.no_unitaryIntertwiner_selectedRepresentation196 completedRootPureState hij.symm W197 intro a198 apply ContinuousLinearMap.ext199 intro x200 simpa [ContinuousLinearMap.comp_apply] using hW a x201 have hVzero : V = 0 :=202 StarAlgHom.Intertwines.eq_zero_of_no_unitary203 (Representation.isIrreducible_starAlgHom tau_j hirrj)204 (Representation.isIrreducible_starAlgHom tau_i hirri)205 hno hV206 apply Submodule.orthogonalProjectionOnto_comp_subtypeL_eq_zero_iff.mp207 simpa [V] using hVzero208209/-- On its own cyclic pure-state piece, the ambient common fixed projection210has image in the distinguished one-dimensional line. This is an ambient-to-211cyclic restriction statement, not an ambient multiplicity claim. -/212theorem initialFixedProjection_maps_ownCyclic213 (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 := by221 let q := transportedFlag family i222 let phi : Limit →L[ℂ] ℂ :=223 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState i).1224 let P : K →L[ℂ] K := commonFixedProjection (fun n ↦ sigma (q n))225 have hPeta : P eta = eta := by226 exact (commonFixedProjection_eq_self_iff (fun n ↦ sigma (q n)) eta).2227 ((mem_commonFixedSubspace_iff (fun n ↦ sigma (q n)) eta).2 hfixed)228 have hoperator (b : Limit) : P * sigma b * P = (phi b) • P := by229 exact commonFixedProjection_comp_map_comp_eq sigma230 (Representation.continuousLinearMap sigma).continuous q phi b231 (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 := by234 have h := congrArg (fun T : K →L[ℂ] K ↦ T eta) (hoperator b)235 simpa [hPeta] using h236 let M := Representation.cyclicSubspace sigma eta237 letI : CompleteSpace M :=238 (Representation.isClosed_cyclicSubspace sigma eta).completeSpace_coe239 let tau := Representation.restrictToReducing sigma M240 (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 eta244 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).continuous248 have hall : ∀ y : M, P (y : K) ∈ (ℂ ∙ eta : Submodule ℂ K) := by249 intro y250 exact hdense.induction_on y hclosed fun b ↦ by251 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⟩255256/-- The common fixed projection for class `i` vanishes on the cyclic piece257of a different selected class `j`. Every nonzero vector in the ambient258fixed range would itself carry class `i`, so orthogonality and the projection259norm identity exclude such a component. -/260theorem initialFixedProjection_eq_zero_on_otherCyclic261 (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 := by270 let q := transportedFlag family i271 let phi : Limit →L[ℂ] ℂ :=272 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState i).1273 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 x276 by_contra hyzero277 have hy_ne : y ≠ 0 := hyzero278 let z : K := NormedSpace.normalize y279 have hz_norm : ‖z‖ = 1 := NormedSpace.norm_normalize hy_ne280 have hy_fixed (n : ℕ) : sigma (q n) y = y := by281 exact commonFixedProjection_apply_fixed (fun n ↦ sigma (q n)) n x282 have hz_fixed (n : ℕ) : sigma (q n) z = z := by283 change sigma (q n) (((‖y‖⁻¹ : ℝ) : ℂ) • y) =284 ((‖y‖⁻¹ : ℝ) : ℂ) • y285 rw [map_smul, hy_fixed]286 have hz_state : Representation.vectorFunctional sigma z = phi := by287 apply vectorFunctional_eq_of_compression_tendsto sigma q phi288 (fun n ↦ (isStarProjection_transportedFlag family i n).isSelfAdjoint.star_eq)289 (tendsto_representative_transported_compression family i)290 z hz_norm hz_fixed291 have horth := isOrtho_cyclicSubspace_of_selectedStates sigma hij z eta_j292 hz_norm heta_j hz_state hstate_j293 have hzx : inner ℂ z x = 0 := horth.inner_eq294 (Representation.self_mem_cyclicSubspace sigma z) hx295 have hy_eq : y = (‖y‖ : ℂ) • z := by296 simpa [z, Complex.real_smul] using (NormedSpace.norm_smul_normalize y).symm297 have hyx : inner ℂ y x = 0 := by298 rw [hy_eq, inner_smul_left, hzx, mul_zero]299 have hnormsq := Submodule.re_inner_starProjection_eq_normSq F x300 change (inner ℂ (P x) x).re = ‖P x‖ ^ 2 at hnormsq301 have hnorm_zero : ‖y‖ ^ 2 = 0 := by302 calc303 ‖y‖ ^ 2 = (inner ℂ y x).re := hnormsq.symm304 _ = 0 := by rw [hyx]; rfl305 exact hy_ne (norm_eq_zero.mp (sq_eq_zero_iff.mp hnorm_zero))306307/-- The cyclic copies of all selected pure states assemble to an isometric308source intertwiner from the displayed arbitrary-index atomic Hilbert sum into309the target Hilbert space. The ambient fixed projection for class `i` maps310the isometry range into the distinguished line carried by the `i`-th selected311vector (and hence back into the isometry range). Surjectivity is deliberately312not asserted here; it is the remaining generated-target reduction step. -/313theorem exists_selectedAtomicCyclicIsometry314 (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 i325 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i)) = eta i) ∧326 (∀ i x, commonFixedProjection327 (fun n ↦ sigma (transportedFlag family i n)) (W x) ∈328 ℂ ∙ eta i) ∧329 ∀ a,330 W.toContinuousLinearMap.comp331 (selectedAtomicRepresentation a) =332 (sigma a).comp333 W.toContinuousLinearMap := by334 classical335 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_coe339 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).comp347 (MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState i a) =348 (tau a).comp349 (U : MathlibAnnex.CStarAlgebra.PureState.SelectedGNS completedRootPureState i →L[ℂ] M i) := by350 simpa [M] using351 exists_selectedCyclicUnitary sigma i (eta i) (heta i) (hstate i)352 choose U hU using hex353 let V (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) :354 MathlibAnnex.CStarAlgebra.PureState.SelectedGNS completedRootPureState i →ₗᵢ[ℂ] K :=355 (M i).subtypeₗᵢ.comp (U i).toLinearIsometry356 have hVortho : OrthogonalFamily ℂ357 (MathlibAnnex.CStarAlgebra.PureState.SelectedGNS completedRootPureState) V := by358 intro i j hij x y359 have horth := isOrtho_cyclicSubspace_of_selectedStates sigma hij360 (eta i) (eta j) (heta i) (heta j) (hstate i) (hstate j)361 exact horth.inner_eq (by362 change (U i x : K) ∈ Representation.cyclicSubspace sigma (eta i)363 exact (U i x).property) (by364 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.linearIsometry368 have hWpoint (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) :369 W (MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState i370 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i)) = eta i := by371 have hsingle := OrthogonalFamily.linearIsometry_apply_single hVortho372 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i)373 calc374 W (MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState i375 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i)) =376 V i (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i) := by377 simpa [W, MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding,378 MathlibAnnex.Analysis.InnerProductSpace.coordinateEmbedding_apply] using hsingle379 _ = eta i := by380 have h := congrArg Subtype.val ((hU i).2.1)381 simpa [V] using h382 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) := by386 have h := congrArg387 (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 h390 simpa [V, ContinuousLinearMap.comp_apply,391 Representation.restrictToReducing_apply_coe] using h'392 refine ⟨W, ?_, ?_, ?_, ?_⟩393 · intro i x394 have hsingle := OrthogonalFamily.linearIsometry_apply_single hVortho x395 have heq : W (MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState i x) =396 V i x := by397 simpa [W, MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding,398 MathlibAnnex.Analysis.InnerProductSpace.coordinateEmbedding_apply] using hsingle399 rw [heq]400 change (U i x : K) ∈ Representation.cyclicSubspace sigma (eta i)401 exact (U i x).property402 · intro i403 exact hWpoint i404 · intro i x405 let P : K →L[ℂ] K := commonFixedProjection406 (fun n ↦ sigma (transportedFlag family i n))407 have hsum : Summable (fun j ↦ V j (x j)) := hVortho.summable_of_lp x408 have hother (j : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) (hji : j ≠ i) :409 P (V j (x j)) = 0 := by410 apply initialFixedProjection_eq_zero_on_otherCyclic family sigma hji.symm411 (eta j) (heta j) (hstate j)412 change (U j (x j) : K) ∈ Representation.cyclicSubspace sigma (eta j)413 exact (U j (x j)).property414 have hcollapse : (∑' j, P (V j (x j))) = P (V i (x i)) := by415 exact tsum_eq_single i hother416 have hfixed_i (n : ℕ) :417 sigma (transportedFlag family i n) (eta i) = eta i := by418 apply projection_apply_eq_self_of_vectorFunctional_eq_one sigma419 (transportedFlag family i n) (isStarProjection_transportedFlag family i n)420 (eta i) (heta i)421 rw [hstate i]422 calc423 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState i).1424 (transportedFlag family i n) = rootState (rootFlag n) :=425 (representativeShellData family i).state_eq (rootFlag n)426 _ = 1 := rootState_rootFlag n427 have hown : P (V i (x i)) ∈ (ℂ ∙ eta i : Submodule ℂ K) := by428 apply initialFixedProjection_maps_ownCyclic family sigma i (eta i)429 hfixed_i430 change (U i (x i) : K) ∈ Representation.cyclicSubspace sigma (eta i)431 exact (U i (x i)).property432 have hPW : P (W x) = P (V i (x i)) := by433 calc434 P (W x) = P (∑' j, V j (x j)) := by435 rw [OrthogonalFamily.linearIsometry_apply hVortho]436 _ = ∑' j, P (V j (x j)) := P.map_tsum hsum437 _ = P (V i (x i)) := hcollapse438 rw [hPW]439 exact hown440 · intro a441 apply ContinuousLinearMap.ext442 intro x443 change W (selectedAtomicRepresentation a x) = sigma a (W x)444 calc445 W (selectedAtomicRepresentation a x) =446 ∑' i, V i ((selectedAtomicRepresentation a x) i) := by447 exact OrthogonalFamily.linearIsometry_apply hVortho _448 _ = ∑' i, V i449 (MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState i a (x i)) := by450 apply tsum_congr451 intro i452 rw [selectedAtomicRepresentation]453 rfl454 _ = ∑' i, sigma a (V i (x i)) := by455 apply tsum_congr456 intro i457 exact hVintertwines i a (x i)458 _ = sigma a (∑' i, V i (x i)) := by459 exact ((sigma a).map_tsum (hVortho.summable_of_lp x)).symm460 _ = sigma a (W x) := by461 rw [OrthogonalFamily.linearIsometry_apply hVortho]462463end MathlibAnnex.CStarAlgebra.CAR