OAI/Analysis/Naimark/Amalgamation.lean

GitHub source file

431 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.NaimarkZFC.IsTracialPositive line 16
  2. theorem OAI.NaimarkZFC.preGNS_norm_star line 19
  3. def OAI.NaimarkZFC.rightMulMapPreGNS line 25
  4. theorem OAI.NaimarkZFC.rightMulMapPreGNS_apply line 40
  5. def OAI.NaimarkZFC.gnsRight line 44
  6. theorem OAI.NaimarkZFC.gnsRight_coe line 47
  7. theorem OAI.NaimarkZFC.gnsLeft_coe line 51
  8. theorem OAI.NaimarkZFC.gnsLeft_commute_right line 56
  9. theorem OAI.NaimarkZFC.gnsRight_star line 65
  10. theorem OAI.NaimarkZFC.gnsRight_mul line 78
  11. def OAI.NaimarkZFC.gnsRightStarAlgHom line 89
  12. theorem OAI.NaimarkZFC.gnsRightStarAlgHom_apply line 123
  13. def OAI.NaimarkZFC.traceVacuum line 126
  14. theorem OAI.NaimarkZFC.traceVacuum_left line 128
  15. theorem OAI.NaimarkZFC.traceVacuum_right line 132
  16. theorem OAI.NaimarkZFC.traceVacuum_cyclic line 136
  17. theorem OAI.NaimarkZFC.traceGNS_injective line 142
  18. theorem OAI.NaimarkZFC.traceRepresentation_injective line 155
  19. theorem OAI.NaimarkZFC.tendsto_zero_of_dense_contractives line 164
  20. theorem OAI.NaimarkZFC.gns_projection_norm line 186
  21. theorem OAI.NaimarkZFC.trace_projection_strong_zero line 192
  22. theorem OAI.NaimarkZFC.trace_projection_right_strong_zero line 210
  23. def OAI.NaimarkZFC.restrictRepresentation line 228
  24. theorem OAI.NaimarkZFC.restrictRepresentation_apply line 247
  25. theorem OAI.NaimarkZFC.gnsRight_projection line 254
  26. def OAI.NaimarkZFC.TraceColumn line 262
  27. instance OAI.NaimarkZFC.traceColumnComplete line 266
  28. theorem OAI.NaimarkZFC.traceColumn_invariant line 271
  29. def OAI.NaimarkZFC.traceColumnRepresentation line 278
  30. def OAI.NaimarkZFC.columnVacuum line 283
  31. theorem OAI.NaimarkZFC.columnVacuum_norm line 287
  32. def OAI.NaimarkZFC.columnUnit line 292
  33. theorem OAI.NaimarkZFC.columnUnit_norm line 296
  34. theorem OAI.NaimarkZFC.columnVacuum_action line 303
  35. theorem OAI.NaimarkZFC.finiteAtomSum_projection line 315
  36. theorem OAI.NaimarkZFC.traceAtoms_jointKernel line 329
  37. theorem OAI.NaimarkZFC.columnAtoms_jointKernel line 348
  38. theorem OAI.NaimarkZFC.columnUnit_ownRow line 359
  39. def OAI.NaimarkZFC.centeredRow line 372
  40. instance OAI.NaimarkZFC.centeredRowComplete line 375
  41. def OAI.NaimarkZFC.vacuumRowFamily line 381
  42. theorem OAI.NaimarkZFC.vacuumRowFamily_orthonormal line 387
  43. theorem OAI.NaimarkZFC.orthogonal_of_basis_inner_zero line 408
  44. def OAI.NaimarkZFC.vacuumRowBasis line 423
  45. theorem OAI.NaimarkZFC.vacuumRowBasis_apply line 457
  46. def OAI.NaimarkZFC.projectionRow line 469
  47. instance OAI.NaimarkZFC.projectionRowComplete line 473
  48. theorem OAI.NaimarkZFC.projectionRow_orthogonal line 479
  49. theorem OAI.NaimarkZFC.projectionRow_total line 496
  50. theorem OAI.NaimarkZFC.projectionRow_eigen line 510
  51. def OAI.NaimarkZFC.hilbertChoiceSet line 526
  52. def OAI.NaimarkZFC.hilbertChoiceBasis line 528
  53. def OAI.NaimarkZFC.CenteredColumn line 533
  54. instance OAI.NaimarkZFC.centeredColumnComplete line 539
  55. abbrev OAI.NaimarkZFC.CenteredColumnIndex line 545
  56. def OAI.NaimarkZFC.tracialColumnBasis line 549
  57. theorem OAI.NaimarkZFC.tracialColumnBasis_none line 562
  58. def OAI.NaimarkZFC.columnVertex line 570
  59. theorem OAI.NaimarkZFC.tracialColumnBasis_row line 574
  60. def OAI.NaimarkZFC.indexedColumnRepresentation line 592
  61. theorem OAI.NaimarkZFC.indexedColumnRepresentation_apply line 604
  62. theorem OAI.NaimarkZFC.indexedColumnRepresentation_atom line 615
  63. theorem OAI.NaimarkZFC.columnUnit_inner_action line 650
  64. theorem OAI.NaimarkZFC.columnUnit_inner_action_zero line 669
  65. theorem OAI.NaimarkZFC.columnUnit_action_norm_sq line 674
  66. theorem OAI.NaimarkZFC.indexedColumnRepresentation_vacuum_vector line 705
  67. theorem OAI.NaimarkZFC.indexedColumnRepresentation_vacuum line 716
  68. theorem OAI.NaimarkZFC.indexedColumnRepresentation_vacuum_norm line 735
  69. theorem OAI.NaimarkZFC.traceRightAtoms_jointKernel line 752
  70. theorem OAI.NaimarkZFC.trace_hasSum_atom_corners line 777
  71. theorem OAI.NaimarkZFC.traceColumn_vacuum_cyclic line 808
  72. theorem OAI.NaimarkZFC.traceColumn_unit_cyclic line 824
  73. inductive OAI.NaimarkZFC.ReducedPath line 851
  74. abbrev OAI.NaimarkZFC.FockIndex line 856
  75. abbrev OAI.NaimarkZFC.FockTail line 858
  76. abbrev OAI.NaimarkZFC.ColumnIndex line 860
  77. abbrev OAI.NaimarkZFC.FockBlockIndex line 862
  78. def OAI.NaimarkZFC.fockJoin line 864
  79. def OAI.NaimarkZFC.fockSplit line 869
  80. theorem OAI.NaimarkZFC.fockJoin_split line 877
  81. theorem OAI.NaimarkZFC.fockSplit_join line 887
  82. def OAI.NaimarkZFC.fockBlockEquiv line 901
  83. def OAI.NaimarkZFC.hilbertBasisReindex line 914
  84. theorem OAI.NaimarkZFC.hilbertBasisReindex_apply line 922
  85. def OAI.NaimarkZFC.l2Basis line 926
  86. theorem OAI.NaimarkZFC.l2Basis_apply line 929
  87. def OAI.NaimarkZFC.l2Reindex line 932
  88. theorem OAI.NaimarkZFC.l2Reindex_apply line 935
  89. theorem OAI.NaimarkZFC.l2Reindex_single line 941
  90. theorem OAI.NaimarkZFC.sumBasis_orthonormal line 957
  91. def OAI.NaimarkZFC.sumHilbertBasis line 971
  92. theorem OAI.NaimarkZFC.sumHilbertBasis_apply line 986
  93. def OAI.NaimarkZFC.l2Sigma line 991
  94. theorem OAI.NaimarkZFC.l2Sigma_apply line 995
  95. def OAI.NaimarkZFC.hilbertSumMap line 1008
  96. theorem OAI.NaimarkZFC.hilbertSumMap_apply line 1024
  97. theorem OAI.NaimarkZFC.hilbertSumMap_norm_le line 1028
  98. theorem OAI.NaimarkZFC.hilbertSumMap_adjoint line 1034
  99. def OAI.NaimarkZFC.hilbertSumRepresentation line 1047
  100. theorem OAI.NaimarkZFC.hilbertSumRepresentation_apply line 1066
  101. abbrev OAI.NaimarkZFC.AtomicFockSpace line 1072
  102. abbrev OAI.NaimarkZFC.FactorBlockSpace line 1073
  103. def OAI.NaimarkZFC.fockBlockUnitary line 1076
  104. theorem OAI.NaimarkZFC.fockBlockUnitary_apply line 1081
  105. theorem OAI.NaimarkZFC.fockBlockUnitary_apply_join line 1088
  106. theorem OAI.NaimarkZFC.fockBlockUnitary_symm_apply line 1093
  107. def OAI.NaimarkZFC.atomicFockRepresentation line 1102
  108. theorem OAI.NaimarkZFC.atomicFockRepresentation_block line 1108
  109. def OAI.NaimarkZFC.fockColumnVertex line 1122
  110. theorem OAI.NaimarkZFC.fockJoin_left line 1127
  111. theorem OAI.NaimarkZFC.atomicFockRepresentation_diagonal line 1135
  112. theorem OAI.NaimarkZFC.atomicFockRepresentation_agree_atoms line 1150
  113. theorem OAI.NaimarkZFC.starAlgHom_ext_closed_adjoin line 1161
  114. def OAI.NaimarkZFC.FockAway line 1176
  115. def OAI.NaimarkZFC.FockStarts line 1179
  116. theorem OAI.NaimarkZFC.fockBlockUnitary_symm_away line 1182
  117. theorem OAI.NaimarkZFC.atomicFock_creation line 1198
  118. theorem OAI.NaimarkZFC.atomicFock_creation_starts line 1210
  119. theorem OAI.NaimarkZFC.atomicFock_creation_norm line 1218
  120. def OAI.NaimarkZFC.fockStartProjection line 1248
  121. theorem OAI.NaimarkZFC.fockStartProjection_apply line 1253
  122. theorem OAI.NaimarkZFC.fockStartProjection_norm_le line 1258
  123. theorem OAI.NaimarkZFC.fockStartProjection_star line 1261
  124. theorem OAI.NaimarkZFC.fockStartProjection_complement_away line 1269
  125. theorem OAI.NaimarkZFC.fockStartProjection_starts line 1274
  126. theorem OAI.NaimarkZFC.fockStartProjection_fix line 1279
  127. theorem OAI.NaimarkZFC.fockStarts_away line 1289
  128. inductive OAI.NaimarkZFC.AlternatingFactorWord line 1298
  129. def OAI.NaimarkZFC.AlternatingFactorWord.eval line 1306
  130. def OAI.NaimarkZFC.AlternatingFactorWord.Centered line 1311
  131. theorem OAI.NaimarkZFC.AlternatingFactorWord.creation line 1315
  132. theorem OAI.NaimarkZFC.AlternatingFactorWord.zero_complement line 1324
  133. def OAI.NaimarkZFC.l2Embed line 1339
  134. theorem OAI.NaimarkZFC.l2Embed_single line 1342
  135. theorem OAI.NaimarkZFC.l2Embed_apply line 1347
  136. theorem OAI.NaimarkZFC.l2Embed_apply_of_not_mem line 1354
  137. def OAI.NaimarkZFC.fockVacuumIndex line 1366
  138. def OAI.NaimarkZFC.fockVacuum line 1370
  139. theorem OAI.NaimarkZFC.fockVacuum_apply_nil line 1372
  140. theorem OAI.NaimarkZFC.fockVacuum_away line 1375
  141. theorem OAI.NaimarkZFC.fockVacuum_norm line 1384
  142. theorem OAI.NaimarkZFC.fockVacuum_inner_starts line 1387
  143. theorem OAI.NaimarkZFC.AlternatingFactorWord.vacuum_zero line 1401
  144. theorem OAI.NaimarkZFC.atomicFock_zero_column line 1415
  145. theorem OAI.NaimarkZFC.fockVacuum_inner line 1441
  146. theorem OAI.NaimarkZFC.atomicFock_vacuum_coeff line 1461
  147. theorem OAI.NaimarkZFC.atomicFock_vacuum_inner line 1470
  148. def OAI.NaimarkZFC.atomicWeightVector line 1485
  149. theorem OAI.NaimarkZFC.atomicWeightVector_apply line 1492
  150. theorem OAI.NaimarkZFC.atomicWeightVector_norm line 1495
  151. def OAI.NaimarkZFC.operatorVectorFunctional line 1509
  152. theorem OAI.NaimarkZFC.operatorVectorFunctional_apply line 1515
  153. theorem OAI.NaimarkZFC.operatorVectorFunctional_star_mul line 1518
  154. theorem OAI.NaimarkZFC.operatorVectorFunctional_star line 1524
  155. theorem OAI.NaimarkZFC.operatorVectorFunctional_norm line 1530
  156. theorem OAI.NaimarkZFC.operatorVectorFunctional_faithful line 1545
  157. structure OAI.NaimarkZFC.AtomicTraceData line 1579
  158. abbrev OAI.NaimarkZFC.AtomicLetters line 1593
  159. abbrev OAI.NaimarkZFC.AtomicHilbertSpace line 1596
  160. def OAI.NaimarkZFC.atomicColumnReps line 1598
  161. def OAI.NaimarkZFC.atomicLeft line 1606
  162. theorem OAI.NaimarkZFC.atomicLeft_atoms line 1609
  163. theorem OAI.NaimarkZFC.atomicLeft_centered line 1619
  164. theorem OAI.NaimarkZFC.atomicLeft_away_norm line 1627
  165. theorem OAI.NaimarkZFC.atomicLeft_injective line 1638
  166. def OAI.NaimarkZFC.atomicVacuum line 1683
  167. theorem OAI.NaimarkZFC.atomicVacuum_norm line 1689
  168. theorem OAI.NaimarkZFC.atomicLeft_vacuum_trace line 1694
  169. structure OAI.NaimarkZFC.IsCenteredWord line 1716
  170. def OAI.NaimarkZFC.wordValue line 1720
  171. theorem OAI.NaimarkZFC.wordValue_nil line 1723
  172. theorem OAI.NaimarkZFC.wordValue_cons line 1725
  173. theorem OAI.NaimarkZFC.IsCenteredWord.tail line 1728
  174. theorem OAI.NaimarkZFC.IsCenteredWord.head line 1732
  175. theorem OAI.NaimarkZFC.IsCenteredWord.modify_head line 1735
  176. theorem OAI.NaimarkZFC.IsCenteredWord.prepend line 1744
  177. structure OAI.NaimarkZFC.CenteredDecomposition line 1756
  178. def OAI.NaimarkZFC.normalSpan line 1762
  179. theorem OAI.NaimarkZFC.normalSpan_diagonal line 1765
  180. theorem OAI.NaimarkZFC.normalSpan_word line 1768
  181. theorem OAI.NaimarkZFC.CenteredDecomposition.diagonal_word_mem line 1773
  182. theorem OAI.NaimarkZFC.CenteredDecomposition.factor_word_mem line 1782
  183. def OAI.NaimarkZFC.leftStabilizer line 1807
  184. theorem OAI.NaimarkZFC.CenteredDecomposition.factor_stabilizes line 1813
  185. theorem OAI.NaimarkZFC.CenteredDecomposition.adjoin_le_normalSpan line 1827
  186. theorem OAI.NaimarkZFC.CenteredDecomposition.diagonal_word_zero line 1844
  187. theorem OAI.NaimarkZFC.CenteredDecomposition.factor_different_zero line 1853
  188. theorem OAI.NaimarkZFC.CenteredDecomposition.factor_long_zero line 1861
  189. def OAI.NaimarkZFC.starWord line 1882
  190. theorem OAI.NaimarkZFC.wordValue_starWord line 1886
  191. theorem OAI.NaimarkZFC.starWord_length line 1897
  192. theorem OAI.NaimarkZFC.IsCenteredWord.starWord line 1903
  193. theorem OAI.NaimarkZFC.CenteredDecomposition.factor_long_zero_right line 1919
  194. theorem OAI.NaimarkZFC.CenteredDecomposition.factor_word_trace line 1929
  195. theorem OAI.NaimarkZFC.CenteredDecomposition.factor_span_trace line 1951
  196. theorem OAI.NaimarkZFC.CenteredDecomposition.adjoin_trace line 1963
  197. def OAI.NaimarkZFC.projectionCorner line 1987
  198. theorem OAI.NaimarkZFC.mem_projectionCorner line 1997
  199. lemma OAI.NaimarkZFC.atom_mul_sum line 2006
  200. lemma OAI.NaimarkZFC.sum_mul_atom line 2020
  201. lemma OAI.NaimarkZFC.atom_mem_finiteCorner line 2033
  202. def OAI.NaimarkZFC.finiteAtomicSpan line 2039
  203. theorem OAI.NaimarkZFC.finiteAtomicSpan_mul line 2043
  204. def OAI.NaimarkZFC.finiteAtomicDiagonal line 2066
  205. theorem OAI.NaimarkZFC.finiteAtomicDiagonal_toSubmodule line 2070
  206. theorem OAI.NaimarkZFC.finiteAtomicDiagonal_le_corner line 2074
  207. theorem OAI.NaimarkZFC.finiteAtomicDiagonal_eigen line 2082
  208. def OAI.NaimarkZFC.atomCornerFunctional line 2105
  209. theorem OAI.NaimarkZFC.atomCornerFunctional_apply line 2110
  210. def OAI.NaimarkZFC.finiteAtomExpectation line 2113
  211. theorem OAI.NaimarkZFC.finiteAtomExpectation_mem line 2116
  212. theorem OAI.NaimarkZFC.finiteAtomExpectation_atom line 2124
  213. theorem OAI.NaimarkZFC.finiteCorner_outside line 2141
  214. theorem OAI.NaimarkZFC.finiteAtomExpectation_centered line 2147
  215. def OAI.NaimarkZFC.finiteFactorCorner line 2157
  216. def OAI.NaimarkZFC.atomicCenteredSubmodule line 2160
  217. theorem OAI.NaimarkZFC.mem_atomicCenteredSubmodule line 2163
  218. theorem OAI.NaimarkZFC.finiteDiagonal_le_factorCorner line 2168
  219. theorem OAI.NaimarkZFC.finiteFactorCorner_decompose line 2181
  220. theorem OAI.NaimarkZFC.finiteDiagonal_mul_centered line 2196
  221. theorem OAI.NaimarkZFC.finiteFactorCorner_star line 2213
  222. theorem OAI.NaimarkZFC.atomicCenteredSubmodule_star line 2223
  223. theorem OAI.NaimarkZFC.finiteCornerCenteredDecomposition line 2245
  224. theorem OAI.NaimarkZFC.finiteCorner_adjoin_trace line 2256
  225. theorem OAI.NaimarkZFC.strong_apply_tendsto line 2290
  226. theorem OAI.NaimarkZFC.strong_mul_tendsto line 2304
  227. def OAI.NaimarkZFC.StronglyApproximable line 2311
  228. theorem OAI.NaimarkZFC.StronglyApproximable.constant line 2318
  229. theorem OAI.NaimarkZFC.StronglyApproximable.add line 2322
  230. theorem OAI.NaimarkZFC.StronglyApproximable.mul line 2332
  231. def OAI.NaimarkZFC.stronglyApproximableAlgebra line 2342
  232. theorem OAI.NaimarkZFC.StronglyApproximable.vector_trace line 2355
  233. theorem OAI.NaimarkZFC.continuous_trace_closure line 2379
  234. def OAI.NaimarkZFC.l2RootTruncation line 2395
  235. theorem OAI.NaimarkZFC.l2RootTruncation_apply line 2418
  236. theorem OAI.NaimarkZFC.l2RootTruncation_norm line 2422
  237. theorem OAI.NaimarkZFC.l2RootTruncation_complement_norm line 2432
  238. theorem OAI.NaimarkZFC.l2RootTruncation_single line 2445
  239. theorem OAI.NaimarkZFC.l2RootTruncation_strong line 2454
  240. abbrev OAI.NaimarkZFC.AtomicOperators line 2488
  241. def OAI.NaimarkZFC.atomicFactor line 2490
  242. def OAI.NaimarkZFC.atomicCommonAtom line 2493
  243. def OAI.NaimarkZFC.atomicState line 2496
  244. theorem OAI.NaimarkZFC.atomicState_apply line 2500
  245. theorem OAI.NaimarkZFC.atomicCommonAtom_idempotent line 2503
  246. theorem OAI.NaimarkZFC.atomicCommonAtom_orthogonal line 2507
  247. theorem OAI.NaimarkZFC.atomicCommonAtom_star line 2511
  248. theorem OAI.NaimarkZFC.atomicCommonAtom_mem line 2515
  249. theorem OAI.NaimarkZFC.atomicCommonAtom_state_ne line 2519
  250. theorem OAI.NaimarkZFC.atomicFactor_star line 2527
  251. theorem OAI.NaimarkZFC.atomicFactor_trace line 2538
  252. theorem OAI.NaimarkZFC.atomicCentered_starts line 2550
  253. theorem OAI.NaimarkZFC.atomicCenteredWord_starts line 2566
  254. theorem OAI.NaimarkZFC.atomicCenteredWord_zero line 2582
  255. theorem OAI.NaimarkZFC.atomicFiniteCorner_trace line 2592
  256. theorem OAI.NaimarkZFC.atomicCommonAtom_apply line 2614
  257. theorem OAI.NaimarkZFC.atomicCommonAtom_sum line 2625
  258. def OAI.NaimarkZFC.atomicFiniteAlgebra line 2633
  259. theorem OAI.NaimarkZFC.atomicFactor_stronglyApproximable line 2637
  260. def OAI.NaimarkZFC.atomicAlgebra line 2681
  261. theorem OAI.NaimarkZFC.atomicAlgebra_stronglyApproximable line 2684
  262. theorem OAI.NaimarkZFC.atomicAlgebra_trace line 2694
  263. def OAI.NaimarkZFC.fockColumnIndexEmbedding line 2708
  264. theorem OAI.NaimarkZFC.fockColumnIndexEmbedding_ne line 2715
  265. theorem OAI.NaimarkZFC.fock_single_away line 2721
  266. theorem OAI.NaimarkZFC.fockColumn_action line 2734
  267. theorem OAI.NaimarkZFC.fock_cyclic_total line 2755
  268. theorem OAI.NaimarkZFC.atomicColumnReps_cyclic line 2799
  269. theorem OAI.NaimarkZFC.atomicCommonAtom_vacuum line 2814
  270. theorem OAI.NaimarkZFC.atomicLeft_mem_algebra line 2847
  271. def OAI.NaimarkZFC.atomicEval line 2850
  272. theorem OAI.NaimarkZFC.atomicAlgebra_cyclic line 2855
  273. def OAI.NaimarkZFC.atomicStarAlgebra line 2877
  274. def OAI.NaimarkZFC.atomicCStarAlgebra line 2896
  275. instance OAI.NaimarkZFC.(instance at line 2899) line 2899
  276. abbrev OAI.NaimarkZFC.AtomicCStar line 2901
  277. def OAI.NaimarkZFC.atomicEmbedding line 2903
  278. theorem OAI.NaimarkZFC.atomicEmbedding_injective line 2907
  279. theorem OAI.NaimarkZFC.atomicCStar_trace line 2911
  280. theorem OAI.NaimarkZFC.atomicCStar_cyclic line 2919
  281. theorem OAI.NaimarkZFC.atomicCStar_faithful line 2925
  282. def OAI.NaimarkZFC.operatorCompression line 2937
  283. theorem OAI.NaimarkZFC.operatorCompression_apply line 2944
  284. theorem OAI.NaimarkZFC.operatorCompression_norm_le line 2948
  285. theorem OAI.NaimarkZFC.operatorCompression_one line 2954
  286. theorem OAI.NaimarkZFC.operatorCompression_inner line 2959
  287. theorem OAI.NaimarkZFC.operatorCompression_zero_of_dense line 2964
  288. theorem OAI.NaimarkZFC.operatorCompression_star line 2983
  289. theorem OAI.NaimarkZFC.faithfulRepresentation_range_closed line 2995
  290. def OAI.NaimarkZFC.representationInverse line 2999
  291. theorem OAI.NaimarkZFC.representationInverse_apply_map line 3011
  292. theorem OAI.NaimarkZFC.representation_map_inverse line 3016
  293. def OAI.NaimarkZFC.cyclicOrbitLinear line 3025
  294. def OAI.NaimarkZFC.cyclicSpan line 3030
  295. instance OAI.NaimarkZFC.cyclicSpanComplete line 3033
  296. theorem OAI.NaimarkZFC.cyclicSpan_invariant line 3036
  297. theorem OAI.NaimarkZFC.cyclicSpan_vector_mem line 3043
  298. def OAI.NaimarkZFC.cyclicOrbit line 3048
  299. theorem OAI.NaimarkZFC.cyclicOrbit_dense line 3051
  300. def OAI.NaimarkZFC.cyclicRepresentation line 3058
  301. theorem OAI.NaimarkZFC.cyclicRepresentation_apply line 3062
  302. theorem OAI.NaimarkZFC.cyclicRepresentation_injective line 3065
  303. def OAI.NaimarkZFC.restrictedVectorFunctional line 3077
  304. theorem OAI.NaimarkZFC.restrictedVectorFunctional_apply line 3084
  305. theorem OAI.NaimarkZFC.restrictedVectorFunctional_norm line 3087
  306. theorem OAI.NaimarkZFC.restrictedVectorFunctional_strict line 3103
  307. def OAI.NaimarkZFC.ambientFactor line 3123
  308. def OAI.NaimarkZFC.factorCompression line 3125
  309. theorem OAI.NaimarkZFC.factorCompression_apply line 3133
  310. theorem OAI.NaimarkZFC.factorCompression_factor line 3137
  311. theorem OAI.NaimarkZFC.factor_word_coefficient line 3146
  312. def OAI.NaimarkZFC.factorAlgebra line 3155
  313. theorem OAI.NaimarkZFC.factorCompression_long_zero line 3166
  314. theorem OAI.NaimarkZFC.factorCompression_different_zero line 3181
  315. theorem OAI.NaimarkZFC.factorCompression_normal_mem line 3201
  316. theorem OAI.NaimarkZFC.factorCompression_star line 3249
  317. theorem OAI.NaimarkZFC.factorCompression_norm_le line 3255
  318. theorem OAI.NaimarkZFC.factorCompression_mul_factor line 3260
  319. theorem OAI.NaimarkZFC.factorCompression_factor_mul line 3266
  320. theorem OAI.NaimarkZFC.factorCompression_vector line 3275
  321. def OAI.NaimarkZFC.cyclicFactorAlgebra line 3283
  322. theorem OAI.NaimarkZFC.factorCompression_mem line 3297
  323. def OAI.NaimarkZFC.compressionIntoFactor line 3306
  324. def OAI.NaimarkZFC.factorExpectation line 3314
  325. theorem OAI.NaimarkZFC.factorExpectation_rep line 3319
  326. theorem OAI.NaimarkZFC.factorExpectation_factor line 3327
  327. theorem OAI.NaimarkZFC.factorExpectation_norm_le line 3332
  328. theorem OAI.NaimarkZFC.factorExpectation_star line 3338
  329. theorem OAI.NaimarkZFC.factorExpectation_mul_factor line 3344
  330. theorem OAI.NaimarkZFC.factorExpectation_factor_mul line 3350
  331. theorem OAI.NaimarkZFC.factorExpectation_trace line 3356
  332. theorem OAI.NaimarkZFC.faithfulStarHom_spectrum line 3370
  333. theorem OAI.NaimarkZFC.faithfulStarHom_nonneg_iff line 3381
  334. theorem OAI.NaimarkZFC.operatorCompression_nonneg line 3402
  335. theorem OAI.NaimarkZFC.factorExpectation_nonneg line 3425
  336. def OAI.NaimarkZFC.factorExpectationPositive line 3435
  337. theorem OAI.NaimarkZFC.atomicCommonAtom_separate line 3452
  338. theorem OAI.NaimarkZFC.atomicLeft_diagonal_agree line 3463
  339. theorem OAI.NaimarkZFC.atomicEmbedding_diagonal_agree line 3474
  340. def OAI.NaimarkZFC.atomicDiagonal line 3478
  341. def OAI.NaimarkZFC.atomicKernel line 3481
  342. theorem OAI.NaimarkZFC.atomicDiagonal_decomposition line 3490
  343. theorem OAI.NaimarkZFC.atomicNormalSpan_dense line 3541
  344. theorem OAI.NaimarkZFC.atomicKernel_starts line 3569
  345. theorem OAI.NaimarkZFC.atomicKernelWord_starts line 3575
  346. theorem OAI.NaimarkZFC.atomicKernelWord_zero line 3592
  347. theorem OAI.NaimarkZFC.atomicFactor_separating line 3603
  348. structure OAI.NaimarkZFC.AtomicAmalgamData line 3621
  349. def OAI.NaimarkZFC.atomicExpectation line 3637
  350. theorem OAI.NaimarkZFC.atomicExpectation_factor line 3647
  351. theorem OAI.NaimarkZFC.atomicExpectation_norm_le line 3651
  352. theorem OAI.NaimarkZFC.atomicExpectation_one line 3655
  353. theorem OAI.NaimarkZFC.atomicExpectation_star line 3658
  354. theorem OAI.NaimarkZFC.atomicExpectation_nonneg line 3662
  355. theorem OAI.NaimarkZFC.atomicExpectation_mul_factor line 3666
  356. theorem OAI.NaimarkZFC.atomicExpectation_factor_mul line 3670
  357. def OAI.NaimarkZFC.atomicTrace line 3674
  358. theorem OAI.NaimarkZFC.atomicTrace_factor line 3678
  359. theorem OAI.NaimarkZFC.atomicTrace_mul line 3683
  360. theorem OAI.NaimarkZFC.atomicTrace_faithful line 3687
  361. theorem OAI.NaimarkZFC.atomicTrace_norm line 3692
  362. theorem OAI.NaimarkZFC.atomicTrace_square line 3696
  363. theorem OAI.NaimarkZFC.atomicTrace_strict line 3707
  364. theorem OAI.NaimarkZFC.atomicExpectation_trace line 3712
  365. theorem OAI.NaimarkZFC.atomicExpectation_faithful line 3717
  366. def OAI.NaimarkZFC.matrixTrace line 3728
  367. theorem OAI.NaimarkZFC.matrixTrace_apply line 3747
  368. theorem OAI.NaimarkZFC.matrixTrace_tracial line 3752
  369. theorem OAI.NaimarkZFC.matrixTrace_faithful line 3764
  370. theorem OAI.NaimarkZFC.matrixTrace_one line 3775
  371. def OAI.NaimarkZFC.normalizedMatrixTrace line 3780
  372. theorem OAI.NaimarkZFC.normalizedMatrixTrace_apply line 3788
  373. theorem OAI.NaimarkZFC.normalizedMatrixTrace_tracial line 3792
  374. theorem OAI.NaimarkZFC.normalizedMatrixTrace_faithful line 3797
  375. theorem OAI.NaimarkZFC.normalizedMatrixTrace_one line 3805
  376. def OAI.NaimarkZFC.matrixSingle line 3815
  377. theorem OAI.NaimarkZFC.matrixSingle_apply line 3819
  378. theorem OAI.NaimarkZFC.matrixSingle_star line 3823
  379. theorem OAI.NaimarkZFC.matrixSingle_mul line 3828
  380. theorem OAI.NaimarkZFC.matrixSingle_mul_of_ne line 3833
  381. theorem OAI.NaimarkZFC.matrixSingle_zero line 3839
  382. theorem OAI.NaimarkZFC.matrixSingle_smul line 3843
  383. theorem OAI.NaimarkZFC.matrixSingle_projection line 3848
  384. theorem OAI.NaimarkZFC.matrixSingle_compress line 3854
  385. def OAI.NaimarkZFC.matrixDiagonalHom line 3859
  386. theorem OAI.NaimarkZFC.matrixDiagonalHom_apply line 3891
  387. theorem OAI.NaimarkZFC.matrixDiagonalHom_mul_apply line 3895
  388. theorem OAI.NaimarkZFC.matrixSingle_diagonal line 3900
  389. def OAI.NaimarkZFC.matrixDiagonalExpectation line 3911
  390. theorem OAI.NaimarkZFC.matrixDiagonalExpectation_apply line 3924
  391. theorem OAI.NaimarkZFC.matrixTrace_single line 3932
  392. theorem OAI.NaimarkZFC.normalizedMatrixTrace_single line 3938
  393. def OAI.NaimarkZFC.matrixAtomicTraceData line 3944
  394. theorem OAI.NaimarkZFC.matrixAtomicTraceData_atom line 3987
  395. structure OAI.NaimarkZFC.MatrixDiagonalInput line 3996
  396. def OAI.NaimarkZFC.matrixInputData line 4017
  397. def OAI.NaimarkZFC.matrixAmalgamData line 4021
  398. theorem OAI.NaimarkZFC.AtomicTraceData.separating line 4058
  399. def OAI.NaimarkZFC.peakAtomicTraceData line 4070
  400. theorem OAI.NaimarkZFC.SequenceDiagonal.tendsto line 4089
  401. def OAI.NaimarkZFC.sequenceDiagonalMap line 4097
  402. theorem OAI.NaimarkZFC.sequenceDiagonalMap_norm_le line 4101
  403. theorem OAI.NaimarkZFC.sequenceDiagonalMap_atom line 4108
  404. theorem OAI.NaimarkZFC.sequenceDiagonalMap_mem line 4118
  405. theorem OAI.NaimarkZFC.sequenceDiagonalMap_atom_right line 4129
  406. theorem OAI.NaimarkZFC.peakAtom_separating line 4146
  407. def OAI.NaimarkZFC.sequenceDiagonalHom line 4153
  408. theorem OAI.NaimarkZFC.sequenceDiagonalHom_injective line 4191
  409. theorem OAI.NaimarkZFC.sequenceDiagonalHom_peakingCoefficients line 4219
  410. theorem OAI.NaimarkZFC.peakingCoefficients_fixes line 4224
  411. theorem OAI.NaimarkZFC.peakingCoefficients_left line 4231
  412. theorem OAI.NaimarkZFC.sequenceDiagonalHom_range line 4241
  413. theorem OAI.NaimarkZFC.peakingCoefficients_zero_corners line 4251
  414. def OAI.NaimarkZFC.positivePullback line 4264
  415. theorem OAI.NaimarkZFC.positivePullback_apply line 4272
  416. def OAI.NaimarkZFC.AtomicTraceData.pullback line 4275
  417. theorem OAI.NaimarkZFC.AtomicTraceData.pullback_atom line 4298
  418. theorem OAI.NaimarkZFC.positiveCLM_isState line 4308
  419. def OAI.NaimarkZFC.peakingMatrixInput line 4320
  420. def OAI.NaimarkZFC.sequenceAtom line 4349
  421. theorem OAI.NaimarkZFC.sequenceDiagonalHom_sequenceAtom line 4352
  422. def OAI.NaimarkZFC.sequenceAtomicTraceData line 4357
  423. theorem OAI.NaimarkZFC.sequenceAtomicTraceData_atom_mul line 4362
  424. def OAI.NaimarkZFC.sequenceMatrixInput line 4371
  425. abbrev OAI.NaimarkZFC.HNNFactor line 4395
  426. instance OAI.NaimarkZFC.(instance at line 4399) line 4399
  427. instance OAI.NaimarkZFC.(instance at line 4402) line 4402
  428. instance OAI.NaimarkZFC.(instance at line 4406) line 4406
  429. def OAI.NaimarkZFC.hnnMatrixInput line 4418
  430. theorem OAI.NaimarkZFC.hnnMatrixInput_weights line 4430
  431. def OAI.NaimarkZFC.hnnAmalgamData line 4445