Exact source: MathlibAnnex/Analysis/CStarAlgebra/CAR/AtomicSource.lean
Pinned GitHub source · Raw UTF-8 source
Back to Shell matching fixes the trace of transported flags
1import MathlibAnnex.Analysis.CStarAlgebra.CAR.DifferenceShell2import MathlibAnnex.Analysis.CStarAlgebra.AtomicConstruction.PureAtomic3import MathlibAnnex.Analysis.CStarAlgebra.Representation.CommonFixedSubspace45/-!6# Completed CAR data for the atomic shell model78The downstream construction is parameterized by one family of shell data.9The historical KOS-facing constructor remains as a compatibility provider;10the closed CAR homogeneity theorem supplies a second provider in `Main`.11-/1213set_option autoImplicit false14set_option maxHeartbeats 8000001516noncomputable section1718open Filter Topology19open scoped ENNReal lp InnerProduct2021namespace MathlibAnnex.CStarAlgebra.CAR2223open MathlibAnnex.Analysis.CStarAlgebra24open MathlibAnnex.Analysis.InnerProductSpace2526/-- Natural source data for one selected pure-state class. Its fields are27only the automorphism and exact algebraic shell links obtained from KOS. -/28structure RepresentativeShellData (j : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) where29 alpha : Limit ≃⋆ₐ[ℂ] Limit30 state_eq : ∀ a : Limit,31 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState j).1 (alpha a) =32 completedRootPureState.1 a33 link : ℕ → Limit34 initial_support : ∀ n,35 star (link n) * link n = alpha (rootShell n)36 final_support : ∀ n,37 link n * star (link n) = rootShell n3839/-- A single fixed family of shell data. The distinguished root component is40definitionally controlled by explicit identity/link equations; no rank-one,41capture, simplicity, or compactness conclusion is stored in this input. -/42structure RepresentativeShellFamily where43 data : ∀ j : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit, RepresentativeShellData j44 root_alpha : (data completedRootPureState.classOf).alpha =45 StarAlgEquiv.refl ℂ Limit46 root_link : ∀ n, (data completedRootPureState.classOf).link n = rootShell n4748/-- The component of a fixed representative shell family. -/49noncomputable def representativeShellData (family : RepresentativeShellFamily)50 (j : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) : RepresentativeShellData j :=51 family.data j5253/-- Historical KOS provider for one component, retained only to build the54compatibility family below. -/55noncomputable def representativeShellDataOfKishimotoOzawaSakai (hKOS : MathlibAnnex.CStarAlgebra.KishimotoOzawaSakaiProperty.{0})56 (j : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) : RepresentativeShellData j := by57 classical58 by_cases hj : j = completedRootPureState.classOf59 · subst j60 exact61 { alpha := StarAlgEquiv.refl ℂ Limit62 state_eq := rootShell_identity_family.163 link := rootShell64 initial_support := fun n ↦ (rootShell_identity_family.2 n).165 final_support := fun n ↦ (rootShell_identity_family.2 n).2 }66 · let hex := exists_representative_rootShell_family_of_kishimotoOzawaSakai hKOS j67 let alpha := Classical.choose hex68 have halpha := Classical.choose_spec hex69 let w := Classical.choose halpha.270 have hw := Classical.choose_spec halpha.271 exact72 { alpha := alpha73 state_eq := halpha.174 link := w75 initial_support := fun n ↦ (hw n).176 final_support := fun n ↦ (hw n).2 }7778/-- Historical all-simple-algebras KOS input produces the same natural family79interface used by the successor construction. -/80noncomputable def representativeShellFamilyOfKishimotoOzawaSakai81 (hKOS : MathlibAnnex.CStarAlgebra.KishimotoOzawaSakaiProperty.{0}) : RepresentativeShellFamily where82 data := representativeShellDataOfKishimotoOzawaSakai hKOS83 root_alpha := by simp [representativeShellDataOfKishimotoOzawaSakai]84 root_link := by85 intro n86 simp [representativeShellDataOfKishimotoOzawaSakai]8788@[simp]89theorem representativeShellData_root_alpha (family : RepresentativeShellFamily) :90 (representativeShellData family completedRootPureState.classOf).alpha =91 StarAlgEquiv.refl ℂ Limit :=92 family.root_alpha9394@[simp]95theorem representativeShellData_root_link (family : RepresentativeShellFamily)96 (n : ℕ) :97 (representativeShellData family completedRootPureState.classOf).link n =98 rootShell n :=99 family.root_link n100101/-- The transported decreasing flag associated with one selected state. -/102noncomputable def transportedFlag (family : RepresentativeShellFamily)103 (j : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) (n : ℕ) : Limit :=104 (representativeShellData family j).alpha (rootFlag n)105106theorem isStarProjection_transportedFlag (family : RepresentativeShellFamily)107 (j : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) (n : ℕ) :108 IsStarProjection (transportedFlag family j n) :=109 (isStarProjection_rootFlag n).map (representativeShellData family j).alpha110111@[simp]112theorem transportedFlag_root (family : RepresentativeShellFamily) (n : ℕ) :113 transportedFlag family completedRootPureState.classOf n = rootFlag n := by114 simp [transportedFlag]115116@[simp]117theorem transportedFlag_zero (family : RepresentativeShellFamily)118 (j : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) : transportedFlag family j 0 = 1 := by119 simp [transportedFlag]120121theorem rootFlag_mul_of_le {m n : ℕ} (hmn : m ≤ n) :122 rootFlag m * rootFlag n = rootFlag n :=123 ((isStarProjection_rootFlag n).le_iff_mul_eq_right124 (isStarProjection_rootFlag m)).1 (antitone_rootFlag hmn)125126theorem transportedFlag_mul_of_le (family : RepresentativeShellFamily)127 (j : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) {m n : ℕ} (hmn : m ≤ n) :128 transportedFlag family j m * transportedFlag family j n =129 transportedFlag family j n := by130 change (representativeShellData family j).alpha (rootFlag m) *131 (representativeShellData family j).alpha (rootFlag n) =132 (representativeShellData family j).alpha (rootFlag n)133 rw [← map_mul, rootFlag_mul_of_le hmn]134135theorem representativeLink_initial (family : RepresentativeShellFamily)136 (j : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) (n : ℕ) :137 star ((representativeShellData family j).link n) *138 (representativeShellData family j).link n =139 transportedFlag family j n - transportedFlag family j (n + 1) := by140 simpa [transportedFlag, rootShell] using141 (representativeShellData family j).initial_support n142143theorem representativeLink_final (family : RepresentativeShellFamily)144 (j : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) (n : ℕ) :145 (representativeShellData family j).link n *146 star ((representativeShellData family j).link n) =147 rootFlag n - rootFlag (n + 1) := by148 simpa [rootShell] using (representativeShellData family j).final_support n149150theorem tendsto_representative_transported_compression151 (family : RepresentativeShellFamily) (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit)152 (b : Limit) :153 Tendsto154 (fun n ↦ transportedFlag family i n * b * transportedFlag family i n -155 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState i).1 b •156 transportedFlag family i n)157 atTop (nhds 0) := by158 exact tendsto_transported_compressionError159 (representativeShellData family i).alpha160 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState i).1161 (representativeShellData family i).state_eq b162163/-- Every transported flag fixes the canonical vector in its matching selected164GNS fiber. -/165theorem selectedVector_fixed_transportedFlag (family : RepresentativeShellFamily)166 (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) (n : ℕ) :167 MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState i168 (transportedFlag family i n)169 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i) =170 MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i := by171 apply projection_apply_eq_self_of_vectorFunctional_eq_one172 (MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState i)173 (transportedFlag family i n) (isStarProjection_transportedFlag family i n)174 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i)175 (MathlibAnnex.CStarAlgebra.PureState.norm_selectedVector completedRootPureState i)176 calc177 Representation.vectorFunctional178 (MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState i)179 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i)180 (transportedFlag family i n) =181 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState i).1182 (transportedFlag family i n) :=183 DFunLike.congr_fun (MathlibAnnex.CStarAlgebra.PureState.selected_vectorFunctional184 completedRootPureState i) _185 _ = rootState (rootFlag n) :=186 (representativeShellData family i).state_eq (rootFlag n)187 _ = 1 := rootState_rootFlag n188189/-- In the matching selected fiber the common fixed projection is the190rank-one projection onto its canonical GNS vector. -/191theorem selected_commonFixedProjection_eq_rankOne192 (family : RepresentativeShellFamily) (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) :193 commonFixedProjection (fun n ↦194 MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState i195 (transportedFlag family i n)) =196 InnerProductSpace.rankOne ℂ197 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i)198 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i) := by199 apply commonFixedProjection_eq_rankOne_of_dense_orbit200 (MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState i)201 (transportedFlag family i)202 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState i).1203 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i)204 · intro n205 exact (isStarProjection_transportedFlag family i n).isSelfAdjoint.star_eq206 · exact tendsto_representative_transported_compression family i207 · exact selectedVector_fixed_transportedFlag family i208 · intro b209 exact (DFunLike.congr_fun (MathlibAnnex.CStarAlgebra.PureState.selected_vectorFunctional210 completedRootPureState i) b).symm211 · exact MathlibAnnex.CStarAlgebra.PureState.denseRange_representative_gns_orbit212 completedRootPureState i213214/-- In every inequivalent selected fiber the same transported flag has zero215common fixed projection. -/216theorem selected_commonFixedProjection_eq_zero217 (family : RepresentativeShellFamily) {i j : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit}218 (hij : j ≠ i) :219 commonFixedProjection (fun n ↦220 MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState j221 (transportedFlag family i n)) = 0 := by222 apply commonFixedProjection_eq_zero_of_no_unitary223 (MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState i)224 (MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState j)225 (transportedFlag family i)226 (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState i).1227 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i)228 · intro n229 exact (isStarProjection_transportedFlag family i n).isSelfAdjoint.star_eq230 · exact tendsto_representative_transported_compression family i231 · intro b232 exact DFunLike.congr_fun (MathlibAnnex.CStarAlgebra.PureState.selected_vectorFunctional233 completedRootPureState i) b234 · exact MathlibAnnex.CStarAlgebra.PureState.denseRange_representative_gns_orbit235 completedRootPureState i236 · exact MathlibAnnex.CStarAlgebra.PureState.isIrreducible_selectedRepresentation237 completedRootPureState j238 · intro U239 exact MathlibAnnex.CStarAlgebra.PureState.no_unitaryIntertwiner_selectedRepresentation240 completedRootPureState hij.symm U241242/-- The transported flag has precisely one fixed coordinate in the displayed243arbitrary-index atomic representation. -/244theorem iInf_range_atomic_transportedFlag_eq_span245 (family : RepresentativeShellFamily) (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) :246 (⨅ n, (atomicRepresentation247 (MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState)248 (transportedFlag family i n)).range) =249 ℂ ∙ MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState i250 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i) := by251 classical252 simpa [MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding] using253 (iInf_range_atomicRepresentation_eq_span254 (MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState)255 (transportedFlag family i)256 (isStarProjection_transportedFlag family i) i257 (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i)258 (MathlibAnnex.CStarAlgebra.PureState.norm_selectedVector completedRootPureState i)259 (selected_commonFixedProjection_eq_rankOne family i)260 (fun j hji ↦ selected_commonFixedProjection_eq_zero family hji))261262end MathlibAnnex.CStarAlgebra.CAR