OAI/Analysis/JiangSu/Model.lean

GitHub source file

487 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Pureness.positive_square_factor line 12
  2. def OAI.Pureness.matrixTraceLinear line 16
  3. lemma OAI.Pureness.matrix_entry_nonneg line 21
  4. def OAI.Pureness.matrixTrace line 28
  5. lemma OAI.Pureness.matrixTrace_apply line 38
  6. lemma OAI.Pureness.matrixTrace_tracial line 41
  7. lemma OAI.Pureness.starAlgHom_positive line 59
  8. def OAI.Pureness.diagonalMatrixHom line 73
  9. lemma OAI.Pureness.diagonalMatrixHom_apply line 81
  10. abbrev OAI.TraceCone.Positive line 91
  11. def OAI.TraceCone.Positive.zero line 103
  12. def OAI.TraceCone.Positive.add line 105
  13. def OAI.TraceCone.Positive.smul line 107
  14. def OAI.TraceCone.Positive.starMul line 110
  15. def OAI.TraceCone.Positive.mulStar line 112
  16. def OAI.TraceCone.Positive.power line 114
  17. def OAI.TraceCone.Positive.rootExponent line 117
  18. structure OAI.TraceCone.ExtendedTrace line 128
  19. instance OAI.TraceCone.ExtendedTrace.(instance at line 147) line 147
  20. def OAI.TraceCone.ExtendedTrace.rank line 149
  21. theorem OAI.TraceCone.ExtendedTrace.ext line 152
  22. instance OAI.TraceCone.ExtendedTrace.(instance at line 158) line 158
  23. instance OAI.TraceCone.ExtendedTrace.(instance at line 166) line 166
  24. theorem OAI.TraceCone.ExtendedTrace.add_apply line 181
  25. instance OAI.TraceCone.ExtendedTrace.(instance at line 184) line 184
  26. theorem OAI.TraceCone.ExtendedTrace.monotone line 191
  27. def OAI.TraceCone.CuntzBelow line 211
  28. def OAI.Pureness.corner line 222
  29. lemma OAI.Pureness.corner_apply_cast line 228
  30. lemma OAI.Pureness.corner_row_zero line 233
  31. lemma OAI.Pureness.corner_col_zero line 237
  32. lemma OAI.Pureness.sum_corner_support line 240
  33. lemma OAI.Pureness.corner_mul line 252
  34. def OAI.Pureness.cornerHom line 263
  35. lemma OAI.Pureness.corner_injective line 280
  36. lemma OAI.Pureness.corner_norm line 287
  37. lemma OAI.Pureness.corner_refl line 291
  38. lemma OAI.Pureness.corner_comp line 296
  39. lemma OAI.Pureness.matrixTrace_corner line 305
  40. def OAI.Pureness.compress line 319
  41. def OAI.Pureness.cornerProjection line 329
  42. lemma OAI.Pureness.cornerProjection_eq line 333
  43. lemma OAI.Pureness.cornerProjection_mul line 344
  44. lemma OAI.Pureness.mul_cornerProjection line 349
  45. lemma OAI.Pureness.corner_compress line 354
  46. def OAI.Pureness.TracialState.comap line 369
  47. abbrev OAI.Pureness.MatrixStage line 389
  48. def OAI.Pureness.matrixConnecting line 391
  49. instance OAI.Pureness.matrixDirectedSystem line 394
  50. abbrev OAI.Pureness.FiniteMatrixLimit line 398
  51. def OAI.Pureness.finiteMatrixInclude line 400
  52. lemma OAI.Pureness.finiteMatrixInclude_corner line 409
  53. def OAI.Pureness.finiteMatrixNorm line 413
  54. lemma OAI.Pureness.finiteMatrixNorm_include line 417
  55. def OAI.Pureness.finiteMatrixGroupNorm line 420
  56. instance OAI.Pureness.finiteMatrixNormedAddCommGroup line 442
  57. instance OAI.Pureness.finiteMatrixTopology line 445
  58. lemma OAI.Pureness.finiteMatrixInclude_norm line 448
  59. instance OAI.Pureness.finiteMatrixNonUnitalNormedRing line 451
  60. instance OAI.Pureness.finiteMatrixModule line 460
  61. instance OAI.Pureness.finiteMatrixNormedSpace line 484
  62. instance OAI.Pureness.finiteMatrixStarRing line 493
  63. instance OAI.Pureness.finiteMatrixCStarRing line 497
  64. instance OAI.Pureness.nonUnitalCompletionMul line 514
  65. instance OAI.Pureness.nonUnitalCompletionContinuousMul line 518
  66. lemma OAI.Pureness.completion_coe_mul line 529
  67. instance OAI.Pureness.nonUnitalCompletionNonUnitalRing line 534
  68. instance OAI.Pureness.nonUnitalCompletionNonUnitalNormedRing line 552
  69. instance OAI.Pureness.nonUnitalCompletionStar line 560
  70. instance OAI.Pureness.nonUnitalCompletionContinuousStar line 562
  71. lemma OAI.Pureness.completion_coe_star line 566
  72. instance OAI.Pureness.nonUnitalCompletionStarRing line 570
  73. instance OAI.Pureness.nonUnitalCompletionCStarRing line 581
  74. instance OAI.Pureness.nonUnitalCompletionStarModule line 587
  75. instance OAI.Pureness.nonUnitalCompletionScalarTower line 593
  76. instance OAI.Pureness.nonUnitalCompletionSMulComm line 602
  77. instance OAI.Pureness.nonUnitalCompletionCStarAlgebra line 611
  78. abbrev OAI.Pureness.CornerCompletion line 620
  79. instance OAI.Pureness.cornerCompletionCStarAlgebra line 622
  80. def OAI.Pureness.completedMatrixInclude line 624
  81. lemma OAI.Pureness.completedMatrixInclude_norm line 632
  82. lemma OAI.Pureness.completedMatrixInclude_isometry line 637
  83. lemma OAI.Pureness.completedMatrixInclude_corner line 640
  84. theorem OAI.Pureness.completedMatrixInclude_dense line 646
  85. instance OAI.Pureness.cornerCompletionOrder line 667
  86. instance OAI.Pureness.cornerCompletionStarOrdered line 669
  87. lemma OAI.Pureness.completedMatrixInclude_nonneg line 671
  88. def OAI.Pureness.completedProjection line 677
  89. lemma OAI.Pureness.completedProjection_star line 679
  90. lemma OAI.Pureness.completedProjection_norm_le line 683
  91. def OAI.Pureness.completedCornerCut line 690
  92. lemma OAI.Pureness.completedCornerCut_continuous line 693
  93. lemma OAI.Pureness.completedCornerCut_sub line 697
  94. lemma OAI.Pureness.completedCornerCut_norm_le line 701
  95. lemma OAI.Pureness.completedCornerCut_fixes line 711
  96. theorem OAI.Pureness.completedCornerCut_tendsto line 718
  97. lemma OAI.Pureness.completedCornerCut_nonneg line 743
  98. abbrev OAI.TraceCone.FinMatrix line 753
  99. def OAI.TraceCone.matrixSuccessor line 756
  100. def OAI.TraceCone.matrixPad line 805
  101. lemma OAI.TraceCone.matrixPad_succ line 809
  102. def OAI.TraceCone.matrixInclusion line 813
  103. lemma OAI.TraceCone.matrixSuccessor_apply_castSucc line 837
  104. lemma OAI.TraceCone.matrixSuccessor_injective line 844
  105. lemma OAI.TraceCone.matrixSuccessor_isometry line 850
  106. lemma OAI.TraceCone.matrixSuccessor_norm line 853
  107. lemma OAI.TraceCone.matrixPad_self line 858
  108. lemma OAI.TraceCone.matrixPad_trans line 862
  109. lemma OAI.TraceCone.matrixInclusion_norm line 866
  110. lemma OAI.TraceCone.matrixInclusion_isometry line 873
  111. lemma OAI.TraceCone.matrixInclusion_trans line 877
  112. abbrev OAI.TraceCone.BoundedFamilies line 890
  113. lemma OAI.TraceCone.BoundedFamilies.norm_coordinate_le line 903
  114. def OAI.TraceCone.BoundedFamilies.vanishing line 906
  115. lemma OAI.TraceCone.BoundedFamilies.mem_vanishing line 916
  116. lemma OAI.TraceCone.BoundedFamilies.mul_mem_vanishing_left line 919
  117. lemma OAI.TraceCone.BoundedFamilies.mul_mem_vanishing_right line 928
  118. lemma OAI.TraceCone.BoundedFamilies.star_mem_vanishing line 937
  119. instance OAI.TraceCone.BoundedFamilies.vanishing_closed line 941
  120. def OAI.TraceCone.BoundedFamilies.vanishingCon line 958
  121. def OAI.TraceCone.FamilyQuotient line 981
  122. instance OAI.TraceCone.FamilyQuotient.(instance at line 995) line 995
  123. instance OAI.TraceCone.FamilyQuotient.(instance at line 998) line 998
  124. instance OAI.TraceCone.FamilyQuotient.(instance at line 1001) line 1001
  125. instance OAI.TraceCone.FamilyQuotient.(instance at line 1004) line 1004
  126. instance OAI.TraceCone.FamilyQuotient.(instance at line 1007) line 1007
  127. def OAI.TraceCone.FamilyQuotient.mk line 1010
  128. lemma OAI.TraceCone.FamilyQuotient.mk_mul line 1012
  129. lemma OAI.TraceCone.FamilyQuotient.mk_surjective line 1014
  130. lemma OAI.TraceCone.FamilyQuotient.mk_eq_mk_iff line 1016
  131. lemma OAI.TraceCone.FamilyQuotient.norm_mk_le line 1019
  132. lemma OAI.TraceCone.FamilyQuotient.exists_norm_mk_lt line 1021
  133. instance OAI.TraceCone.FamilyQuotient.(instance at line 1024) line 1024
  134. instance OAI.TraceCone.FamilyQuotient.(instance at line 1038) line 1038
  135. lemma OAI.TraceCone.FamilyQuotient.mk_star line 1045
  136. instance OAI.TraceCone.FamilyQuotient.(instance at line 1047) line 1047
  137. instance OAI.TraceCone.FamilyQuotient.(instance at line 1063) line 1063
  138. instance OAI.TraceCone.FamilyQuotient.(instance at line 1069) line 1069
  139. instance OAI.TraceCone.FamilyQuotient.(instance at line 1076) line 1076
  140. lemma OAI.TraceCone.BoundedFamilies.norm_bounded line 1094
  141. lemma OAI.TraceCone.BoundedFamilies.norm_cobounded line 1098
  142. lemma OAI.TraceCone.BoundedFamilies.limsup_norm_nonneg line 1103
  143. lemma OAI.TraceCone.BoundedFamilies.limsup_norm_le_of_vanishing_sub line 1107
  144. def OAI.TraceCone.BoundedFamilies.tail line 1121
  145. lemma OAI.TraceCone.BoundedFamilies.tail_sub_mem line 1129
  146. lemma OAI.TraceCone.BoundedFamilies.norm_tail_le line 1136
  147. theorem OAI.TraceCone.FamilyQuotient.norm_mk_eq_limsup line 1157
  148. lemma OAI.TraceCone.FamilyQuotient.norm_star_mul_self_eq line 1174
  149. instance OAI.TraceCone.FamilyQuotient.(instance at line 1192) line 1192
  150. instance OAI.TraceCone.FamilyQuotient.(instance at line 1195) line 1195
  151. def OAI.TraceCone.matrixFamily line 1207
  152. def OAI.TraceCone.FamilyQuotient.quotientHom line 1250
  153. lemma OAI.TraceCone.FamilyQuotient.mk_eq_of_eventually_eq line 1258
  154. def OAI.TraceCone.matrixStage line 1275
  155. lemma OAI.TraceCone.matrixStage_norm line 1278
  156. lemma OAI.TraceCone.matrixStage_compatible line 1288
  157. def OAI.TraceCone.matrixUnion line 1304
  158. def OAI.TraceCone.matrixLimitAlgebra line 1322
  159. instance OAI.TraceCone.matrixLimitAlgebra_closed line 1325
  160. abbrev OAI.TraceCone.MatrixLimit line 1328
  161. instance OAI.TraceCone.(instance at line 1330) line 1330
  162. def OAI.TraceCone.matrixLimitStage line 1342
  163. lemma OAI.TraceCone.matrixLimitStage_norm line 1350
  164. lemma OAI.TraceCone.matrixLimitStage_isometry line 1353
  165. lemma OAI.TraceCone.matrixLimitStage_compatible line 1356
  166. theorem OAI.TraceCone.matrixLimit_finite_approximation line 1360
  167. def OAI.TraceCone.extendDenseStarHom line 1375
  168. theorem OAI.TraceCone.extendDenseStarHom_eq line 1402
  169. def OAI.TraceCone.finiteMatrixSubalgebra line 1416
  170. def OAI.TraceCone.finiteMatrixStage line 1419
  171. lemma OAI.TraceCone.finiteMatrixStage_surjective line 1422
  172. lemma OAI.TraceCone.finiteMatrixSubalgebra_dense line 1427
  173. def OAI.TraceCone.finiteMatrixRepresentative line 1434
  174. lemma OAI.TraceCone.finiteMatrixRepresentative_spec line 1437
  175. def OAI.TraceCone.finiteMatrixLiftValue line 1452
  176. lemma OAI.TraceCone.finiteMatrixLiftValue_eq line 1456
  177. lemma OAI.TraceCone.finiteMatrixLiftValue_stage line 1468
  178. lemma OAI.TraceCone.finiteMatrix_common_stage line 1472
  179. def OAI.TraceCone.finiteMatrixLift line 1480
  180. lemma OAI.TraceCone.finiteMatrixLift_norm_le line 1503
  181. def OAI.TraceCone.matrixLimitLift line 1509
  182. theorem OAI.TraceCone.matrixLimitLift_stage line 1513
  183. lemma OAI.Pureness.shared_matrixSuccessor_eq_corner line 1528
  184. lemma OAI.Pureness.shared_matrixInclusion_eq_corner line 1541
  185. lemma OAI.Pureness.completedMatrixInclude_shared_compatible line 1549
  186. def OAI.Pureness.sharedMatrixToCompletion line 1553
  187. lemma OAI.Pureness.sharedMatrixToCompletion_stage line 1556
  188. lemma OAI.Pureness.sharedMatrixToCompletion_continuous line 1560
  189. lemma OAI.Pureness.sharedMatrixToCompletion_norm line 1567
  190. lemma OAI.Pureness.sharedMatrixToCompletion_isometry line 1577
  191. lemma OAI.Pureness.sharedMatrixToCompletion_surjective line 1580
  192. def OAI.Pureness.sharedMatrixEquiv line 1593
  193. def OAI.TraceCone.Positive.map line 1605
  194. def OAI.TraceCone.ExtendedTrace.pullback line 1619
  195. instance OAI.TraceCone.(instance at line 1654) line 1654
  196. instance OAI.TraceCone.(instance at line 1656) line 1656
  197. lemma OAI.Pureness.completedCornerCut_finite_range line 1665
  198. theorem OAI.Pureness.completedCornerCut_mem_range line 1675
  199. def OAI.Pureness.completedCompress line 1686
  200. lemma OAI.Pureness.include_completedCompress line 1689
  201. lemma OAI.Pureness.completedCompress_continuous line 1693
  202. lemma OAI.Pureness.completedCompress_include line 1697
  203. theorem OAI.Pureness.nonUnitalStarAlgHom_nonneg_iff line 1709
  204. lemma OAI.Pureness.matrixTrace_compress_le line 1737
  205. lemma OAI.Pureness.completedCompress_nonneg line 1747
  206. lemma OAI.Pureness.completedProjection_mul_le line 1754
  207. lemma OAI.Pureness.completedProjection_mul_ge line 1760
  208. lemma OAI.Pureness.completedCornerCut_nested line 1766
  209. lemma OAI.Pureness.completedCornerCut_include line 1774
  210. theorem OAI.Pureness.completedCompress_compat line 1779
  211. lemma OAI.Pureness.completedCompression_trace_monotone line 1785
  212. lemma OAI.Pureness.completedCornerCut_add line 1799
  213. lemma OAI.Pureness.completedCornerCut_smul line 1803
  214. def OAI.Pureness.completedCompressLinear line 1807
  215. lemma OAI.Pureness.completedCompress_mono line 1818
  216. lemma OAI.Pureness.completedCompress_include_of_le line 1825
  217. def OAI.Pureness.completedTraceValue line 1830
  218. def OAI.Pureness.completedDiagonalWeight line 1833
  219. lemma OAI.Pureness.completedTraceValue_continuous line 1836
  220. lemma OAI.Pureness.completedTraceValue_mono line 1841
  221. lemma OAI.Pureness.completedTraceValue_monotone line 1846
  222. lemma OAI.Pureness.completedDiagonalWeight_tendsto line 1852
  223. lemma OAI.Pureness.completedDiagonalWeight_mono line 1856
  224. lemma OAI.Pureness.completedTraceValue_add line 1860
  225. theorem OAI.Pureness.completedDiagonalWeight_add line 1871
  226. theorem OAI.Pureness.completedDiagonalWeight_include line 1879
  227. theorem OAI.Pureness.completedDiagonalWeight_le_of_tendsto line 1893
  228. lemma OAI.Pureness.completedDiagonalWeight_cut line 1901
  229. lemma OAI.Pureness.completedDiagonalWeight_cut_le line 1906
  230. lemma OAI.Pureness.completedProjection_conjugate_le line 1911
  231. lemma OAI.Pureness.completedCornerCut_mono line 1921
  232. lemma OAI.Pureness.completedCornerCut_mul_star_le line 1926
  233. lemma OAI.Pureness.completedDiagonalWeight_finite_polar line 1936
  234. lemma OAI.Pureness.completedDiagonalWeight_star_mul_le line 1943
  235. theorem OAI.Pureness.completedDiagonalWeight_tracial line 1952
  236. lemma OAI.Pureness.completedTraceValue_smul line 1963
  237. lemma OAI.Pureness.completedDiagonalWeight_smul line 1970
  238. lemma OAI.Pureness.completedDiagonalWeight_zero line 1974
  239. def OAI.Pureness.nonUnitalNormalize line 1986
  240. def OAI.Pureness.nonUnitalRoot line 1988
  241. def OAI.Pureness.completedRootRank line 1998
  242. abbrev OAI.Pureness.CStarAlgebraNorm.normedRing line 2007
  243. def OAI.Pureness.CStarAlgebraNorm.normedAlgebra line 2010
  244. theorem OAI.Pureness.CStarAlgebraNorm.cstarRing line 2016
  245. def OAI.DirectComparison.StrictComparison line 2029
  246. def OAI.DirectComparison.UniformGamma line 2033
  247. class OAI.DirectPacking.TraceFamily line 2050
  248. abbrev OAI.DirectPacking.RestrictedTracialState line 2053
  249. abbrev OAI.DirectPacking.RestrictedTracialState.functional line 2064
  250. lemma OAI.DirectPacking.RestrictedTracialState.normalized line 2066
  251. lemma OAI.DirectPacking.RestrictedTracialState.tracial line 2068
  252. def OAI.NonunitalGamma.positiveFunctionalCLM line 2079
  253. structure OAI.NonunitalGamma.NormalizedTrace line 2082
  254. lemma OAI.NonunitalGamma.positiveFunctional_cauchy_schwarz line 2087
  255. lemma OAI.NonunitalGamma.positiveFunctional_norm_le_sqrt line 2093
  256. lemma OAI.NonunitalGamma.positiveFunctional_norm_sq_le line 2112
  257. def OAI.NonunitalGamma.unitizedFunctionalLinear line 2119
  258. lemma OAI.NonunitalGamma.unitizedFunctional_star_square line 2124
  259. def OAI.NonunitalGamma.unitizedFunctional line 2145
  260. lemma OAI.NonunitalGamma.unitizedFunctional_one line 2156
  261. lemma OAI.NonunitalGamma.unitizedFunctional_tracial line 2161
  262. def OAI.NonunitalGamma.NormalizedTrace.toWeakDual line 2176
  263. instance OAI.NonunitalGamma.(instance at line 2179) line 2179
  264. def OAI.NonunitalGamma.NormalizedTrace.unitized line 2189
  265. def OAI.NonunitalGamma.WeightBounded line 2201
  266. def OAI.NonunitalGamma.WeightDenselyFinite line 2204
  267. lemma OAI.NonunitalGamma.weightBounded_finite line 2207
  268. def OAI.NonunitalGamma.ExtendedTraceExtension.value line 2235
  269. lemma OAI.NonunitalGamma.ExtendedTraceExtension.value_nonneg line 2237
  270. lemma OAI.NonunitalGamma.ExtendedTraceExtension.value_zero line 2239
  271. lemma OAI.NonunitalGamma.ExtendedTraceExtension.value_add line 2242
  272. lemma OAI.NonunitalGamma.ExtendedTraceExtension.value_smul line 2245
  273. def OAI.NonunitalGamma.ExtendedTraceExtension.selfAdjointValue line 2249
  274. lemma OAI.NonunitalGamma.ExtendedTraceExtension.selfAdjointValue_sub line 2253
  275. lemma OAI.NonunitalGamma.ExtendedTraceExtension.selfAdjointValue_add line 2265
  276. lemma OAI.NonunitalGamma.ExtendedTraceExtension.selfAdjointValue_smul_nonneg line 2279
  277. lemma OAI.NonunitalGamma.ExtendedTraceExtension.selfAdjointValue_neg line 2290
  278. lemma OAI.NonunitalGamma.ExtendedTraceExtension.selfAdjointValue_smul line 2297
  279. lemma OAI.NonunitalGamma.ExtendedTraceExtension.selfAdjointValue_positive line 2307
  280. def OAI.NonunitalGamma.ExtendedTraceExtension.realLinear line 2313
  281. def OAI.NonunitalGamma.ExtendedTraceExtension.complexLinear line 2318
  282. lemma OAI.NonunitalGamma.ExtendedTraceExtension.complexLinear_positive line 2326
  283. def OAI.NonunitalGamma.ExtendedTraceExtension.functional line 2334
  284. lemma OAI.NonunitalGamma.ExtendedTraceExtension.functional_positive line 2339
  285. lemma OAI.NonunitalGamma.ExtendedTraceExtension.linearMap_tracial_of_star_mul line 2343
  286. lemma OAI.NonunitalGamma.ExtendedTraceExtension.functional_tracial line 2358
  287. def OAI.NonunitalGamma.boundedWeightFunctional line 2373
  288. lemma OAI.NonunitalGamma.boundedWeightFunctional_tracial line 2376
  289. def OAI.NonunitalGamma.scaleFunctional line 2387
  290. lemma OAI.NonunitalGamma.scaleFunctional_apply line 2393
  291. lemma OAI.NonunitalGamma.positiveFunctionalCLM_scale line 2396
  292. lemma OAI.NonunitalGamma.scaleFunctional_norm line 2401
  293. lemma OAI.NonunitalGamma.boundedWeightFunctional_nonzero line 2407
  294. def OAI.NonunitalGamma.normalizedWeight line 2420
  295. def OAI.NonunitalGamma.TopologicallySimple line 2435
  296. def OAI.NonunitalGamma.Projectionless line 2446
  297. def OAI.Pureness.completedExtendedTrace line 2458
  298. def OAI.Pureness.sharedExtendedTrace line 2471
  299. def OAI.NonunitalGamma.finiteMatrixMap line 2483
  300. lemma OAI.NonunitalGamma.finiteMatrixMap_successor line 2487
  301. lemma OAI.NonunitalGamma.finiteMatrixMap_inclusion line 2496
  302. lemma OAI.NonunitalGamma.stabilizationCompatible line 2503
  303. def OAI.NonunitalGamma.stabilizationMap line 2510
  304. def OAI.NonunitalGamma.stabilizationInr line 2513
  305. def OAI.NonunitalGamma.NormalizedTrace.stabilized line 2516
  306. def OAI.NonunitalGamma.scaledTrace line 2526
  307. def OAI.NonunitalGamma.boundedStabilized line 2535
  308. def OAI.NonunitalGamma.AllDenselyFiniteTracesBounded line 2542
  309. def OAI.NonunitalGamma.StrictComparison line 2546
  310. def OAI.NonunitalGamma.UniformGamma line 2560
  311. def OAI.NonunitalGamma.StablyProjectionless line 2578
  312. structure OAI.NuclearUnitization.NonUnitalCStarNorm line 2587
  313. def OAI.NuclearUnitization.IsNuclear line 2592
  314. abbrev OAI.Pureness.CStarAlgebraNorm.Completion line 2600
  315. instance OAI.Pureness.CStarAlgebraNorm.completionCStarAlgebra line 2604
  316. structure OAI.ConcreteMatrixUnits.System line 2616
  317. abbrev OAI.JiangSuConstruction.Mat line 2627
  318. abbrev OAI.JiangSuConstruction.TensorMat line 2629
  319. abbrev OAI.JiangSuConstruction.Interval line 2631
  320. def OAI.JiangSuConstruction.leftAmplification line 2640
  321. def OAI.JiangSuConstruction.rightAmplification line 2662
  322. def OAI.JiangSuConstruction.evalHom line 2684
  323. def OAI.JiangSuConstruction.leftEndpoint line 2693
  324. def OAI.JiangSuConstruction.rightEndpoint line 2695
  325. def OAI.JiangSuConstruction.dimensionDrop line 2697
  326. instance OAI.JiangSuConstruction.tensorMat_finiteDimensional line 2701
  327. lemma OAI.JiangSuConstruction.leftAmplification_closed line 2705
  328. lemma OAI.JiangSuConstruction.rightAmplification_closed line 2709
  329. instance OAI.JiangSuConstruction.dimensionDrop_closed line 2713
  330. abbrev OAI.JiangSuConstruction.DimensionDrop line 2726
  331. instance OAI.JiangSuConstruction.(instance at line 2728) line 2728
  332. def OAI.SequentialCStar.boundedOne line 2742
  333. instance OAI.SequentialCStar.(instance at line 2746) line 2746
  334. lemma OAI.SequentialCStar.quotient_one_mul line 2748
  335. lemma OAI.SequentialCStar.quotient_mul_one line 2756
  336. instance OAI.SequentialCStar.(instance at line 2764) line 2764
  337. instance OAI.SequentialCStar.(instance at line 2768) line 2768
  338. instance OAI.SequentialCStar.(instance at line 2776) line 2776
  339. instance OAI.SequentialCStar.(instance at line 2778) line 2778
  340. instance OAI.SequentialCStar.(instance at line 2782) line 2782
  341. instance OAI.SequentialCStar.(instance at line 2785) line 2785
  342. structure OAI.SequentialCStar.System line 2788
  343. lemma OAI.SequentialCStar.System.map_norm line 2807
  344. def OAI.SequentialCStar.System.family line 2810
  345. def OAI.SequentialCStar.System.stageNonUnital line 2838
  346. lemma OAI.SequentialCStar.System.stageNonUnital_norm line 2841
  347. lemma OAI.SequentialCStar.System.stageNonUnital_one line 2851
  348. def OAI.SequentialCStar.System.stage line 2857
  349. lemma OAI.SequentialCStar.System.stage_norm line 2867
  350. lemma OAI.SequentialCStar.System.stage_compatible line 2869
  351. def OAI.SequentialCStar.System.unionAlgebra line 2878
  352. def OAI.SequentialCStar.System.limitAlgebra line 2897
  353. instance OAI.SequentialCStar.System.limitAlgebra_closed line 2899
  354. abbrev OAI.SequentialCStar.System.Limit line 2902
  355. instance OAI.SequentialCStar.System.(instance at line 2904) line 2904
  356. def OAI.SequentialCStar.System.inclusion line 2906
  357. lemma OAI.SequentialCStar.System.inclusion_norm line 2915
  358. lemma OAI.SequentialCStar.System.inclusion_isometry line 2917
  359. theorem OAI.SequentialCStar.System.finite_stage_approximation line 2919
  360. def OAI.SequentialCStar.sequenceHom line 2934
  361. lemma OAI.SequentialCStar.sequenceHom_self line 2938
  362. lemma OAI.SequentialCStar.sequenceHom_succ line 2942
  363. lemma OAI.SequentialCStar.sequenceHom_comp line 2947
  364. lemma OAI.SequentialCStar.sequenceHom_injective line 2954
  365. def OAI.SequentialCStar.System.ofSequence line 2963
  366. structure OAI.JiangSuConstruction.Multiplicities line 2973
  367. def OAI.JiangSuConstruction.lowerEigenvalue line 2998
  368. def OAI.JiangSuConstruction.upperEigenvalue line 3002
  369. theorem OAI.JiangSuConstruction.midpoint_value_mem line 3006
  370. def OAI.JiangSuConstruction.midpoint line 3009
  371. lemma OAI.JiangSuConstruction.matrix_finite_spectrum line 3016
  372. lemma OAI.JiangSuConstruction.finite_spectrum_unitary_exp line 3020
  373. lemma OAI.JiangSuConstruction.finite_matrix_unitary_joined_one line 3034
  374. def OAI.JiangSuConstruction.finiteMatrixUnitaryPath line 3039
  375. def OAI.JiangSuConstruction.blockDiagonalHom line 3048
  376. lemma OAI.JiangSuConstruction.blockDiagonalHom_apply line 3060
  377. lemma OAI.JiangSuConstruction.blockDiagonalHom_injective line 3064
  378. lemma OAI.JiangSuConstruction.blockDiagonalHom_continuous line 3070
  379. def OAI.JiangSuConstruction.diagonalContinuousHom line 3073
  380. def OAI.JiangSuConstruction.unitaryConjugation line 3084
  381. lemma OAI.JiangSuConstruction.unitaryConjugation_injective line 3096
  382. def OAI.JiangSuConstruction.continuousUnitaryConjugation line 3102
  383. lemma OAI.JiangSuConstruction.continuousUnitaryConjugation_injective line 3114
  384. def OAI.JiangSuConstruction.endpointLeftEquiv line 3127
  385. def OAI.JiangSuConstruction.endpointRightEquiv line 3138
  386. def OAI.JiangSuConstruction.endpointReduced line 3158
  387. lemma OAI.JiangSuConstruction.endpoint_left_regroup line 3164
  388. def OAI.JiangSuConstruction.endpointRightReduced line 3201
  389. lemma OAI.JiangSuConstruction.endpoint_right_regroup line 3207
  390. def OAI.JiangSuConstruction.continuousReindex line 3250
  391. lemma OAI.JiangSuConstruction.continuousReindex_injective line 3255
  392. def OAI.JiangSuConstruction.connectingAmbient line 3269
  393. lemma OAI.JiangSuConstruction.connectingAmbient_zero line 3276
  394. lemma OAI.JiangSuConstruction.connectingAmbient_one line 3286
  395. def OAI.JiangSuConstruction.connectingMap line 3296
  396. def OAI.JiangSuConstruction.permutationUnitary line 3324
  397. lemma OAI.JiangSuConstruction.permutationUnitary_conjugation line 3334
  398. lemma OAI.JiangSuConstruction.reindex_trans line 3355
  399. lemma OAI.JiangSuConstruction.reindex_blockDiagonal line 3359
  400. lemma OAI.JiangSuConstruction.reindex_kronecker line 3371
  401. lemma OAI.JiangSuConstruction.reindex_left_amplification line 3378
  402. lemma OAI.JiangSuConstruction.reindex_right_amplification line 3387
  403. lemma OAI.JiangSuConstruction.permutation_after_reindex line 3396
  404. structure OAI.OriginalJiangSu.Pair line 3409
  405. structure OAI.OriginalJiangSu.Multiplicities line 3416
  406. lemma OAI.OriginalJiangSu.mod_pos_of_coprime line 3448
  407. lemma OAI.OriginalJiangSu.arithmetic_multiplicities line 3454
  408. lemma OAI.OriginalJiangSu.multiplicities_exists line 3500
  409. def OAI.OriginalJiangSu.multiplicities line 3516
  410. def OAI.OriginalJiangSu.Pair.next line 3519
  411. def OAI.OriginalJiangSu.pair line 3524
  412. abbrev OAI.OriginalJiangSu.Index line 3534
  413. def OAI.OriginalJiangSu.family line 3536
  414. def OAI.OriginalJiangSu.sumSwapFirst line 3541
  415. def OAI.OriginalJiangSu.zeroCountEquiv line 3547
  416. def OAI.OriginalJiangSu.zeroMidEquiv line 3550
  417. def OAI.OriginalJiangSu.oneCountEquiv line 3554
  418. def OAI.OriginalJiangSu.oneMidEquiv line 3557
  419. def OAI.OriginalJiangSu.zeroBlockEquiv line 3561
  420. def OAI.OriginalJiangSu.oneBlockEquiv line 3565
  421. lemma OAI.OriginalJiangSu.family_zero line 3569
  422. lemma OAI.OriginalJiangSu.family_one line 3579
  423. lemma OAI.OriginalJiangSu.family_cover line 3589
  424. def OAI.OriginalJiangSu.zeroReducedEquiv line 3608
  425. def OAI.OriginalJiangSu.zeroTensorEquiv line 3612
  426. def OAI.OriginalJiangSu.oneReducedEquiv line 3615
  427. def OAI.OriginalJiangSu.oneTensorEquiv line 3619
  428. def OAI.OriginalJiangSu.zeroIndexEquiv line 3622
  429. def OAI.OriginalJiangSu.oneIndexEquiv line 3627
  430. lemma OAI.OriginalJiangSu.zeroIndex_endpoint line 3632
  431. lemma OAI.OriginalJiangSu.oneIndex_endpoint line 3664
  432. def OAI.OriginalJiangSu.step line 3696
  433. lemma OAI.OriginalJiangSu.diagonalContinuousHom_injective_cover line 3704
  434. lemma OAI.OriginalJiangSu.connectingAmbient_injective_cover line 3715
  435. theorem OAI.OriginalJiangSu.step_injective line 3722
  436. abbrev OAI.OriginalJiangSu.Stage line 3734
  437. instance OAI.OriginalJiangSu.stageNontrivial line 3744
  438. def OAI.OriginalJiangSu.stageStep line 3749
  439. lemma OAI.OriginalJiangSu.stageStep_injective line 3751
  440. def OAI.OriginalJiangSu.system line 3753
  441. abbrev OAI.OriginalJiangSu.Algebra line 3756
  442. instance OAI.OriginalJiangSu.limitNontrivial line 3758
  443. instance OAI.OriginalJiangSu.algebraOrder line 3761
  444. instance OAI.OriginalJiangSu.algebraStarOrder line 3763
  445. theorem OAI.SequentialCStar.System.exists_dense_stage_sequence line 3772
  446. instance OAI.OriginalJiangSu.algebraSeparable line 3810
  447. structure OAI.FourEdgeSurgery.Flow line 3819
  448. instance OAI.FourEdgeSurgery.(instance at line 3824) line 3824
  449. lemma OAI.FourEdgeSurgery.Flow.map_add line 3826
  450. def OAI.Pureness.commutingTensorClosure line 3836
  451. instance OAI.Pureness.commutingTensorClosure_closed line 3839
  452. instance OAI.Pureness.commutingTensorClosureCStarAlgebra line 3842
  453. def OAI.NonunitalTensor.elementarySet line 3852
  454. def OAI.NonunitalTensor.coefficientSpan line 3854
  455. lemma OAI.NonunitalTensor.coefficientSpan_mem line 3856
  456. lemma OAI.NonunitalTensor.span_mul_mem line 3869
  457. lemma OAI.NonunitalTensor.span_star_mem line 3892
  458. def OAI.NonunitalTensor.coefficientAlgebra line 3902
  459. def OAI.NonunitalTensor.tensorIdeal line 3910
  460. instance OAI.NonunitalTensor.tensorIdeal_closed line 3912
  461. instance OAI.NonunitalTensor.(instance at line 3915) line 3915
  462. def OAI.NonunitalTensor.originalHom line 3925
  463. lemma OAI.NonunitalTensor.original_commute line 3928
  464. def OAI.ActualHilbertTensor.TensorSpace line 3937
  465. instance OAI.ActualHilbertTensor.normedAddCommGroup line 3939
  466. instance OAI.ActualHilbertTensor.innerProductSpace line 3942
  467. instance OAI.ActualHilbertTensor.completeSpace line 3945
  468. def OAI.ActualSpatial.Hilbert line 3956
  469. instance OAI.ActualSpatial.hilbertNormedAddCommGroup line 3958
  470. instance OAI.ActualSpatial.hilbertInnerProductSpace line 3962
  471. instance OAI.ActualSpatial.hilbertCompleteSpace line 3966
  472. abbrev OAI.ActualSpatial.Op line 3970
  473. abbrev OAI.ActualSpatial.repA line 3972
  474. def OAI.ActualSpatial.leftAction line 3974
  475. def OAI.ActualSpatial.rightAction line 3976
  476. lemma OAI.ActualSpatial.commute line 3978
  477. abbrev OAI.ActualSpatial.Tensor line 3981
  478. instance OAI.ActualSpatial.(instance at line 3983) line 3983
  479. instance OAI.ActualSpatial.(instance at line 3985) line 3985
  480. def OAI.ActualSpatial.leftHom line 3987
  481. def OAI.ActualSpatial.rightHom line 3991
  482. lemma OAI.ActualSpatial.homs_commute line 3995
  483. lemma OAI.ActualSpatial.commuting_range_eq_span line 4008
  484. instance OAI.ActualSpatial.tensorSeparable line 4025
  485. abbrev OAI.ActualSpatial.nonunitalIdeal line 4047
  486. def OAI.ActualSpatial.NonunitalTensor line 4053
  487. instance OAI.ActualSpatial.(instance at line 4055) line 4055