OAI/Analysis/Naimark/HNN.lean

GitHub source file

215 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.NaimarkZFC.PeakingPairData.Corner line 15
  2. instance OAI.NaimarkZFC.PeakingPairData.modelCornerCStarAlgebra line 16
  3. abbrev OAI.NaimarkZFC.PeakingPairData.cornerBase line 17
  4. theorem OAI.NaimarkZFC.PeakingPairData.cornerBase_injective line 19
  5. theorem OAI.NaimarkZFC.PeakingPairData.corner_unique line 22
  6. theorem OAI.NaimarkZFC.PeakingPairData.corner_unique_pure_extension line 26
  7. abbrev OAI.NaimarkZFC.PeakingPairData.stableUnitary line 32
  8. theorem OAI.NaimarkZFC.PeakingPairData.stable_conjugates_peak line 36
  9. def OAI.NaimarkZFC.matrixCornerEntry line 50
  10. theorem OAI.NaimarkZFC.matrixCornerEntry_coe line 63
  11. theorem OAI.NaimarkZFC.matrixCornerEntry_corner line 67
  12. theorem OAI.NaimarkZFC.matrix_diag_sum_one line 72
  13. theorem OAI.NaimarkZFC.matrixCornerEntry_mul line 77
  14. theorem OAI.NaimarkZFC.matrixCornerEntry_star line 98
  15. theorem OAI.NaimarkZFC.matrixSingle_sandwich line 105
  16. theorem OAI.NaimarkZFC.matrixCornerEntry_base line 120
  17. theorem OAI.NaimarkZFC.matrixCornerEntry_one line 127
  18. def OAI.NaimarkZFC.matrixEntrySubalgebra line 138
  19. theorem OAI.NaimarkZFC.mem_matrixEntrySubalgebra line 156
  20. theorem OAI.NaimarkZFC.matrixEntrySubalgebra_closed line 159
  21. theorem OAI.NaimarkZFC.matrixCorner_generated_of_entries line 167
  22. theorem OAI.NaimarkZFC.matrixCornerEntry_letter_false line 188
  23. theorem OAI.NaimarkZFC.matrixCornerEntry_letter_true line 216
  24. def OAI.NaimarkZFC.matrixCornerLetter line 224
  25. theorem OAI.NaimarkZFC.matrixCornerLetter_star line 227
  26. theorem OAI.NaimarkZFC.matrixCorner_generators line 239
  27. abbrev OAI.NaimarkZFC.PeakingPairData.cornerLetter line 281
  28. theorem OAI.NaimarkZFC.PeakingPairData.cornerLetter_true line 285
  29. theorem OAI.NaimarkZFC.PeakingPairData.cornerLetter_false line 286
  30. theorem OAI.NaimarkZFC.PeakingPairData.cornerLetter_star line 287
  31. theorem OAI.NaimarkZFC.PeakingPairData.corner_generated line 290
  32. def OAI.NaimarkZFC.matrixCornerExpectation line 304
  33. theorem OAI.NaimarkZFC.matrixCornerExpectation_apply line 308
  34. theorem OAI.NaimarkZFC.matrixCornerExpectation_base line 311
  35. theorem OAI.NaimarkZFC.matrixCornerExpectation_one line 316
  36. theorem OAI.NaimarkZFC.matrixCornerExpectation_norm line 321
  37. theorem OAI.NaimarkZFC.matrixCornerExpectation_star line 325
  38. theorem OAI.NaimarkZFC.matrixCornerExpectation_supported line 332
  39. theorem OAI.NaimarkZFC.matrixCornerExpectation_faithful line 347
  40. theorem OAI.NaimarkZFC.matrixCornerExpectation_state line 359
  41. abbrev OAI.NaimarkZFC.PeakingPairData.modelExpectation line 380
  42. def OAI.NaimarkZFC.PeakingPairData.expectCorner line 383
  43. theorem OAI.NaimarkZFC.PeakingPairData.expectCorner_base line 386
  44. theorem OAI.NaimarkZFC.PeakingPairData.expectCorner_one line 390
  45. theorem OAI.NaimarkZFC.PeakingPairData.expectCorner_norm line 394
  46. theorem OAI.NaimarkZFC.PeakingPairData.expectCorner_star line 398
  47. theorem OAI.NaimarkZFC.PeakingPairData.expectCorner_faithful line 402
  48. theorem OAI.NaimarkZFC.PeakingPairData.expectCorner_state line 408
  49. theorem OAI.NaimarkZFC.matrixCornerLetter_coe line 423
  50. def OAI.NaimarkZFC.HNNWord.matrixCore line 440
  51. def OAI.NaimarkZFC.HNNWord.matrixFinal line 444
  52. theorem OAI.NaimarkZFC.HNNWord.eval_matrix_core line 448
  53. theorem OAI.NaimarkZFC.HNNWord.matrixCore_centered line 475
  54. theorem OAI.NaimarkZFC.atomicFock_vacuum_away_ne line 493
  55. theorem OAI.NaimarkZFC.fockAway_inner_starts line 504
  56. theorem OAI.NaimarkZFC.atomicCore_coefficient_zero line 525
  57. theorem OAI.NaimarkZFC.atomicCore_coe line 536
  58. theorem OAI.NaimarkZFC.atomicExpectation_core_zero line 552
  59. theorem OAI.NaimarkZFC.atomicExpectation_sandwich_core_zero line 573
  60. def OAI.NaimarkZFC.PeakingPairData.turnCentered line 589
  61. theorem OAI.NaimarkZFC.PeakingPairData.turn_matrix_centered line 591
  62. theorem OAI.NaimarkZFC.PeakingPairData.modelExpectation_hnn_word line 610
  63. theorem OAI.NaimarkZFC.PeakingPairData.expectCorner_hnn_word line 627
  64. def OAI.NaimarkZFC.cornerTrace line 642
  65. theorem OAI.NaimarkZFC.cornerTrace_apply line 645
  66. theorem OAI.NaimarkZFC.cornerTrace_isState line 648
  67. theorem OAI.NaimarkZFC.cornerTrace_tracial line 657
  68. theorem OAI.NaimarkZFC.cornerTrace_faithful line 662
  69. abbrev OAI.NaimarkZFC.PeakingPairData.modelTrace line 678
  70. theorem OAI.NaimarkZFC.PeakingPairData.modelTrace_isState line 680
  71. theorem OAI.NaimarkZFC.PeakingPairData.modelTrace_base line 683
  72. def OAI.NaimarkZFC.PeakingPairData.traceCorner line 687
  73. theorem OAI.NaimarkZFC.PeakingPairData.traceCorner_base line 691
  74. theorem OAI.NaimarkZFC.PeakingPairData.traceCorner_isState line 697
  75. theorem OAI.NaimarkZFC.PeakingPairData.traceCorner_tracial line 703
  76. theorem OAI.NaimarkZFC.PeakingPairData.traceCorner_faithful line 706
  77. theorem OAI.NaimarkZFC.PeakingPairData.traceCorner_strict line 710
  78. theorem OAI.NaimarkZFC.PeakingPairData.traceCorner_faithfulTracial line 720
  79. theorem OAI.NaimarkZFC.matrixCorner_trace_expectation line 732
  80. theorem OAI.NaimarkZFC.PeakingPairData.traceCorner_expectation line 753
  81. theorem OAI.NaimarkZFC.PeakingPairData.traceCorner_hnn_word line 760
  82. theorem OAI.NaimarkZFC.hnn_reverse_conjugacy line 771
  83. theorem OAI.NaimarkZFC.hnn_turn_split line 782
  84. theorem OAI.NaimarkZFC.matrixCornerLetter_diagonal line 799
  85. theorem OAI.NaimarkZFC.PeakingPairData.cornerLetter_diagonal line 817
  86. def OAI.NaimarkZFC.PeakingPairData.turnCenter line 822
  87. def OAI.NaimarkZFC.PeakingPairData.turnRemainder line 825
  88. theorem OAI.NaimarkZFC.PeakingPairData.turnCenter_centered line 828
  89. theorem OAI.NaimarkZFC.PeakingPairData.cornerLetter_turn line 833
  90. theorem OAI.NaimarkZFC.PeakingPairData.corner_restriction line 849
  91. theorem OAI.NaimarkZFC.PeakingPairData.corner_restriction_expectation line 871
  92. def OAI.NaimarkZFC.PeakingPairData.HNNAlgebra line 893
  93. instance OAI.NaimarkZFC.PeakingPairData.hnnCStar line 894
  94. instance OAI.NaimarkZFC.PeakingPairData.hnnOrder line 897
  95. instance OAI.NaimarkZFC.PeakingPairData.hnnStarOrder line 900
  96. def OAI.NaimarkZFC.PeakingPairData.hnnBase line 904
  97. def OAI.NaimarkZFC.PeakingPairData.hnnLetter line 905
  98. def OAI.NaimarkZFC.PeakingPairData.hnnTrace line 906
  99. def OAI.NaimarkZFC.PeakingPairData.hnnExpectation line 907
  100. theorem OAI.NaimarkZFC.PeakingPairData.hnnBase_injective line 909
  101. theorem OAI.NaimarkZFC.PeakingPairData.hnnLetter_star line 910
  102. theorem OAI.NaimarkZFC.PeakingPairData.hnnLetter_turn line 912
  103. theorem OAI.NaimarkZFC.PeakingPairData.hnn_generated line 916
  104. theorem OAI.NaimarkZFC.PeakingPairData.hnnTrace_isState line 919
  105. theorem OAI.NaimarkZFC.PeakingPairData.hnnTrace_base line 920
  106. theorem OAI.NaimarkZFC.PeakingPairData.hnnTrace_faithful line 921
  107. theorem OAI.NaimarkZFC.PeakingPairData.hnnTrace_tracial line 923
  108. theorem OAI.NaimarkZFC.PeakingPairData.hnnExpectation_base line 925
  109. theorem OAI.NaimarkZFC.PeakingPairData.hnnExpectation_word line 926
  110. theorem OAI.NaimarkZFC.PeakingPairData.hnnTrace_expectation line 928
  111. def OAI.NaimarkZFC.cornerRestrictState line 938
  112. theorem OAI.NaimarkZFC.cornerRestrictState_apply line 942
  113. theorem OAI.NaimarkZFC.cornerRestrictState_isState line 947
  114. theorem OAI.NaimarkZFC.cornerLift_restrict line 952
  115. theorem OAI.NaimarkZFC.cornerLiftState_isPureState line 957
  116. theorem OAI.NaimarkZFC.pureState_equivalent_of_conjugate line 983
  117. theorem OAI.NaimarkZFC.Peaks.join_extensions line 1016
  118. def OAI.NaimarkZFC.PureStateEquivalent line 1048
  119. theorem OAI.NaimarkZFC.Peaks.join_named line 1053
  120. theorem OAI.NaimarkZFC.no_common_irrep_of_state_decay line 1072
  121. theorem OAI.NaimarkZFC.map_cross_decay line 1095
  122. theorem OAI.NaimarkZFC.bridge_cross_decay line 1110
  123. theorem OAI.NaimarkZFC.PeakingPairData.Endpoint.cross_decay line 1142
  124. theorem OAI.NaimarkZFC.PeakingPairData.Endpoint.disjoint_matrix_irrep line 1153
  125. theorem OAI.NaimarkZFC.PeakingPairData.exists_endpoint_representative line 1182
  126. theorem OAI.NaimarkZFC.equivalent_pure_coefficient_vector line 1212
  127. theorem OAI.NaimarkZFC.pureGNS_equivalent_of_state_eq line 1244
  128. theorem OAI.NaimarkZFC.PeakingPairData.matrix_no_unintended_join line 1256
  129. def OAI.NaimarkZFC.cornerUnitary line 1304
  130. theorem OAI.NaimarkZFC.cornerUnitary_apply line 1317
  131. theorem OAI.NaimarkZFC.cornerCompression_conjugate line 1320
  132. theorem OAI.NaimarkZFC.cornerLift_equivalence line 1349
  133. theorem OAI.NaimarkZFC.corner_extensions_inequivalent_of_matrix_no_common line 1372
  134. def OAI.NaimarkZFC.PeakingPairData.hnnUnitary line 1406
  135. theorem OAI.NaimarkZFC.PeakingPairData.hnnUnitary_conjugates line 1408
  136. theorem OAI.NaimarkZFC.PeakingPairData.hnn_unique line 1412
  137. theorem OAI.NaimarkZFC.PeakingPairData.hnn_join line 1416
  138. theorem OAI.NaimarkZFC.PeakingPairData.hnn_no_unintended_join line 1425
  139. theorem OAI.NaimarkZFC.matrixCornerExpectation_nonneg line 1456
  140. theorem OAI.NaimarkZFC.exists_pure_norming_state line 1470
  141. theorem OAI.NaimarkZFC.positive_eq_zero_of_pure_states line 1517
  142. theorem OAI.NaimarkZFC.exists_contracting_real_dual line 1531
  143. def OAI.NaimarkZFC.idealSelfAdjointSubspace line 1539
  144. theorem OAI.NaimarkZFC.properIdeal_one_sub_norm line 1550
  145. theorem OAI.NaimarkZFC.exists_state_killing_ideal line 1560
  146. theorem OAI.NaimarkZFC.gns_vector_zero_of_square_zero line 1618
  147. theorem OAI.NaimarkZFC.gns_kills_ideal line 1624
  148. theorem OAI.NaimarkZFC.simple_extension_of_uep_expectation line 1641
  149. theorem OAI.NaimarkZFC.simple_extension_of_uep_square_expectation line 1700
  150. theorem OAI.NaimarkZFC.PeakingPairData.expectCorner_square_nonneg line 1720
  151. theorem OAI.NaimarkZFC.PeakingPairData.corner_simple line 1726
  152. theorem OAI.NaimarkZFC.matrixCornerExpectation_left line 1739
  153. theorem OAI.NaimarkZFC.matrixCornerExpectation_right line 1747
  154. theorem OAI.NaimarkZFC.PeakingPairData.hnnExpectation_left line 1760
  155. theorem OAI.NaimarkZFC.PeakingPairData.hnnExpectation_right line 1766
  156. theorem OAI.NaimarkZFC.PeakingPairData.hnnExpectation_square_nonneg line 1772
  157. theorem OAI.NaimarkZFC.PeakingPairData.hnnExpectation_faithful line 1775
  158. theorem OAI.NaimarkZFC.PeakingPairData.hnn_simple line 1778
  159. theorem OAI.NaimarkZFC.pure_lifts_equivalent line 1789
  160. def OAI.NaimarkZFC.PureUEP line 1821
  161. theorem OAI.NaimarkZFC.restrictState_comp line 1824
  162. theorem OAI.NaimarkZFC.PureUEP.comp line 1829
  163. theorem OAI.NaimarkZFC.PureUEP.id line 1850
  164. theorem OAI.NaimarkZFC.PureUEP.of_dense_cover line 1860
  165. theorem OAI.NaimarkZFC.simple_of_dense_stage_ranges line 1892
  166. theorem OAI.NaimarkZFC.StateExtensionUnique.postcomp_equiv line 1936
  167. theorem OAI.NaimarkZFC.PureUEP.postcomp_equiv line 1951
  168. theorem OAI.NaimarkZFC.IsSimpleCStar.of_equiv line 1955
  169. theorem OAI.NaimarkZFC.pureUEP_ordinal_chain line 1975
  170. inductive OAI.NaimarkZFC.BridgeSuccessor line 2030
  171. theorem OAI.NaimarkZFC.BridgeSuccessor.properties line 2036
  172. theorem OAI.NaimarkZFC.bridge_ordinal_simple line 2065
  173. theorem OAI.NaimarkZFC.bridge_ordinal_pureUEP line 2081
  174. theorem OAI.NaimarkZFC.StateExtensionUnique.of_surjective line 2096
  175. theorem OAI.NaimarkZFC.isPureState_restrict_equiv line 2106
  176. theorem OAI.NaimarkZFC.pureStateEquivalent_restrict_equiv line 2117
  177. theorem OAI.NaimarkZFC.mixed_zero_of_state_cross_decay line 2138
  178. theorem OAI.NaimarkZFC.pureExcisionNet_value line 2157
  179. theorem OAI.NaimarkZFC.inequivalent_pure_mixed_zero line 2164
  180. theorem OAI.NaimarkZFC.pure_inequivalent_of_dense_restrictions line 2205
  181. theorem OAI.NaimarkZFC.pure_inequivalent_ordinal_chain line 2242
  182. theorem OAI.NaimarkZFC.Peaks.extend line 2299
  183. theorem OAI.NaimarkZFC.Peaks.restrict line 2313
  184. def OAI.NaimarkZFC.PeakingPairData.pushedState line 2360
  185. theorem OAI.NaimarkZFC.PeakingPairData.pushedState_isPure line 2363
  186. theorem OAI.NaimarkZFC.PeakingPairData.pushedState_restrict line 2366
  187. def OAI.NaimarkZFC.PeakingPairData.push line 2370
  188. def OAI.NaimarkZFC.PeakingPairData.hnnPush line 2390
  189. theorem OAI.NaimarkZFC.PeakingPairData.hnn_restriction line 2406
  190. theorem OAI.NaimarkZFC.PeakingPairData.hnn_restriction_expectation line 2429
  191. def OAI.NaimarkZFC.HNNWord.lastCoefficient line 2448
  192. def OAI.NaimarkZFC.HNNWord.mapCoefficients line 2452
  193. theorem OAI.NaimarkZFC.HNNWord.first_mapCoefficients line 2456
  194. theorem OAI.NaimarkZFC.HNNWord.last_mapCoefficients line 2459
  195. theorem OAI.NaimarkZFC.HNNWord.mapCoefficients_reduced line 2465
  196. theorem OAI.NaimarkZFC.HNNWord.eval_mapCoefficients line 2473
  197. def OAI.NaimarkZFC.HNNWord.join line 2479
  198. theorem OAI.NaimarkZFC.HNNWord.first_join line 2483
  199. theorem OAI.NaimarkZFC.HNNWord.last_join line 2486
  200. theorem OAI.NaimarkZFC.HNNWord.join_reduced line 2492
  201. theorem OAI.NaimarkZFC.HNNWord.eval_join line 2500
  202. def OAI.NaimarkZFC.hnnBaseTailSpan line 2512
  203. theorem OAI.NaimarkZFC.hnnBaseTailSpan_contains_word line 2516
  204. theorem OAI.NaimarkZFC.hnnBaseTailSpan_mul_center_word line 2525
  205. theorem OAI.NaimarkZFC.PeakingPairData.hnn_inclusion line 2564
  206. theorem OAI.NaimarkZFC.PeakingPairData.peakAtom_separates line 2615
  207. theorem OAI.NaimarkZFC.PeakingPairData.diagonal_atom line 2619
  208. theorem OAI.NaimarkZFC.PeakingPairData.expectation_nat line 2623
  209. theorem OAI.NaimarkZFC.PeakingPairData.expectation_infty line 2628
  210. theorem OAI.NaimarkZFC.PeakingPairData.atom_natural line 2634
  211. theorem OAI.NaimarkZFC.PeakingPairData.state_natural line 2639
  212. theorem OAI.NaimarkZFC.PeakingPairData.diagonal_natural line 2647
  213. theorem OAI.NaimarkZFC.PeakingPairData.expectation_natural line 2655
  214. theorem OAI.NaimarkZFC.PeakingPairData.hnn_inclusion_of_peaks line 2668
  215. theorem OAI.NaimarkZFC.PeakingPairData.hnn_equiv_of_peaks line 2685