OAI/Analysis/Naimark/Peaking.lean

GitHub source file

205 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.NaimarkZFC.matrixSingle_add line 13
  2. def OAI.NaimarkZFC.matrixCornerProjection line 20
  3. theorem OAI.NaimarkZFC.matrixCornerProjection_isProjection line 22
  4. abbrev OAI.NaimarkZFC.MatrixHNNCorner line 25
  5. def OAI.NaimarkZFC.matrixCornerBase line 28
  6. theorem OAI.NaimarkZFC.matrixCornerBase_coe line 53
  7. theorem OAI.NaimarkZFC.matrixCornerBase_injective line 56
  8. def OAI.NaimarkZFC.matrixStableElement line 66
  9. theorem OAI.NaimarkZFC.matrixStableElement_mem line 69
  10. def OAI.NaimarkZFC.matrixStable line 77
  11. theorem OAI.NaimarkZFC.matrixStable_star_mul line 80
  12. theorem OAI.NaimarkZFC.matrixStable_mul_star line 90
  13. def OAI.NaimarkZFC.matrixStableUnitary line 99
  14. theorem OAI.NaimarkZFC.matrixDiagonalHom_single line 102
  15. theorem OAI.NaimarkZFC.matrixDiagonal_agrees line 112
  16. theorem OAI.NaimarkZFC.matrixDiagonal_units line 119
  17. theorem OAI.NaimarkZFC.matrixStable_conjugates line 125
  18. def OAI.NaimarkZFC.matrixSingleHom line 155
  19. theorem OAI.NaimarkZFC.matrixSingleHom_apply line 164
  20. def OAI.NaimarkZFC.matrixSinglePositive line 167
  21. def OAI.NaimarkZFC.matrixEntryPositive line 179
  22. def OAI.NaimarkZFC.matrixEntryCLM line 195
  23. def OAI.NaimarkZFC.matrixSingleCLM line 200
  24. def OAI.NaimarkZFC.matrixState line 205
  25. theorem OAI.NaimarkZFC.matrixState_apply line 209
  26. theorem OAI.NaimarkZFC.matrixState_isState line 212
  27. theorem OAI.NaimarkZFC.matrix_state_supported line 221
  28. theorem OAI.NaimarkZFC.matrix_corner_isState line 230
  29. theorem OAI.NaimarkZFC.Peaks.matrix line 239
  30. def OAI.NaimarkZFC.matrixTraceState line 263
  31. theorem OAI.NaimarkZFC.matrixTraceState_isState line 266
  32. theorem OAI.NaimarkZFC.matrixTraceState_tracial line 276
  33. theorem OAI.NaimarkZFC.matrixTraceState_single line 282
  34. theorem OAI.NaimarkZFC.matrix_peakAtom line 287
  35. theorem OAI.NaimarkZFC.matrix_cornerState line 291
  36. theorem OAI.NaimarkZFC.matrix_peakAtom_positive line 305
  37. theorem OAI.NaimarkZFC.matrix_peakingCoefficients line 310
  38. theorem OAI.NaimarkZFC.matrix_endpoint_decay line 330
  39. theorem OAI.NaimarkZFC.two_end_norm_bound line 357
  40. theorem OAI.NaimarkZFC.fockStartProjection_isProjection line 381
  41. theorem OAI.NaimarkZFC.atomicLeft_start_bound line 394
  42. theorem OAI.NaimarkZFC.atomicCoordinate_norm_le line 421
  43. theorem OAI.NaimarkZFC.atomicExpectation_corner_formula line 440
  44. theorem OAI.NaimarkZFC.atomicLeft_expectation_bound line 450
  45. theorem OAI.NaimarkZFC.atomicLeft_expectation_bound_right line 463
  46. theorem OAI.NaimarkZFC.two_end_tendsto line 478
  47. theorem OAI.NaimarkZFC.atomicLeft_endpoint_tendsto line 507
  48. theorem OAI.NaimarkZFC.atomicLeft_endpoint_tendsto_right line 517
  49. theorem OAI.NaimarkZFC.atomic_core_endpoint_decay line 528
  50. def OAI.NaimarkZFC.matrixPeakingExpectation line 554
  51. theorem OAI.NaimarkZFC.matrix_excision_square_endpoint line 558
  52. theorem OAI.NaimarkZFC.matrix_centered_state_zero line 586
  53. theorem OAI.NaimarkZFC.Peaks.rectangular_excision line 598
  54. inductive OAI.NaimarkZFC.BridgeCore line 628
  55. def OAI.NaimarkZFC.BridgeCore.left line 635
  56. def OAI.NaimarkZFC.BridgeCore.right line 638
  57. def OAI.NaimarkZFC.BridgeCore.Centered line 641
  58. def OAI.NaimarkZFC.BridgeCore.eval line 647
  59. def OAI.NaimarkZFC.BridgeCore.cons line 652
  60. theorem OAI.NaimarkZFC.BridgeCore.eval_cons line 657
  61. theorem OAI.NaimarkZFC.BridgeCore.centered_cons line 664
  62. def OAI.NaimarkZFC.BridgeCore.snoc line 671
  63. theorem OAI.NaimarkZFC.BridgeCore.eval_snoc line 676
  64. theorem OAI.NaimarkZFC.BridgeCore.centered_snoc line 683
  65. theorem OAI.NaimarkZFC.BridgeCore.left_cons line 690
  66. theorem OAI.NaimarkZFC.BridgeCore.right_cons line 692
  67. theorem OAI.NaimarkZFC.BridgeCore.left_snoc line 694
  68. theorem OAI.NaimarkZFC.BridgeCore.right_snoc line 696
  69. theorem OAI.NaimarkZFC.BridgeCore.left_support line 702
  70. theorem OAI.NaimarkZFC.BridgeCore.right_support line 705
  71. theorem OAI.NaimarkZFC.BridgeCore.creation line 719
  72. theorem OAI.NaimarkZFC.BridgeCore.zero_complement line 739
  73. def OAI.NaimarkZFC.bridgeWordSet line 757
  74. def OAI.NaimarkZFC.bridgeWordSpan line 760
  75. theorem OAI.NaimarkZFC.bridgeWordSpan_base line 762
  76. theorem OAI.NaimarkZFC.bridgeWordSpan_word line 765
  77. theorem OAI.NaimarkZFC.bridgeWordSpan_letter line 769
  78. theorem OAI.NaimarkZFC.bridgeWordSpan_mul_base line 773
  79. theorem OAI.NaimarkZFC.bridgeWordSpan_mul_base_right line 784
  80. theorem OAI.NaimarkZFC.bridgeWordSpan_left_word line 799
  81. theorem OAI.NaimarkZFC.bridgeWordSpan_mul_letter line 832
  82. theorem OAI.NaimarkZFC.adjoin_le_bridgeWordSpan line 844
  83. def OAI.NaimarkZFC.bridgeLetter line 882
  84. def OAI.NaimarkZFC.bridgeSupport line 884
  85. theorem OAI.NaimarkZFC.bridgeLetter_support_left line 888
  86. theorem OAI.NaimarkZFC.bridgeLetter_support_right line 895
  87. theorem OAI.NaimarkZFC.bridgeSupport_norm line 900
  88. theorem OAI.NaimarkZFC.bridgeLetter_star line 905
  89. theorem OAI.NaimarkZFC.bridgeLetter_transfer line 911
  90. theorem OAI.NaimarkZFC.matrixSingle_diagonal_general line 918
  91. theorem OAI.NaimarkZFC.matrix_offdiagonal_turn line 929
  92. theorem OAI.NaimarkZFC.bridgeLetter_diagonal_turn line 945
  93. def OAI.NaimarkZFC.bridgeCenter line 953
  94. theorem OAI.NaimarkZFC.bridgeCenter_centered line 958
  95. theorem OAI.NaimarkZFC.bridgeLetter_turn line 963
  96. theorem OAI.NaimarkZFC.matrix_bridge_adjoin_le_span line 973
  97. theorem OAI.NaimarkZFC.AtomicAmalgamData.left_agree line 989
  98. theorem OAI.NaimarkZFC.AtomicAmalgamData.core_zero line 995
  99. theorem OAI.NaimarkZFC.peakingCoefficients_peak_nat line 1013
  100. theorem OAI.NaimarkZFC.peakingCoefficients_peak_eq line 1022
  101. theorem OAI.NaimarkZFC.sequenceDiagonalHom_matched_peak line 1033
  102. structure OAI.NaimarkZFC.PeakingPairData line 1046
  103. def OAI.NaimarkZFC.PeakingPairData.input line 1066
  104. def OAI.NaimarkZFC.PeakingPairData.atoms line 1070
  105. def OAI.NaimarkZFC.PeakingPairData.amalgam line 1072
  106. abbrev OAI.NaimarkZFC.PeakingPairData.Model line 1075
  107. instance OAI.NaimarkZFC.PeakingPairData.modelCStarAlgebra line 1077
  108. instance OAI.NaimarkZFC.PeakingPairData.modelAddZeroClass line 1079
  109. abbrev OAI.NaimarkZFC.PeakingPairData.Operators line 1082
  110. abbrev OAI.NaimarkZFC.PeakingPairData.base line 1083
  111. abbrev OAI.NaimarkZFC.PeakingPairData.aux line 1084
  112. abbrev OAI.NaimarkZFC.PeakingPairData.diagonal line 1085
  113. abbrev OAI.NaimarkZFC.PeakingPairData.expectation line 1086
  114. theorem OAI.NaimarkZFC.PeakingPairData.amalgam_diagonal_false line 1088
  115. theorem OAI.NaimarkZFC.PeakingPairData.amalgam_diagonal_true line 1090
  116. theorem OAI.NaimarkZFC.PeakingPairData.diagonal_agree line 1093
  117. theorem OAI.NaimarkZFC.PeakingPairData.expectation_eq line 1101
  118. theorem OAI.NaimarkZFC.PeakingPairData.expectation_fixes line 1105
  119. theorem OAI.NaimarkZFC.PeakingPairData.letter_centered line 1108
  120. abbrev OAI.NaimarkZFC.PeakingPairData.letter line 1118
  121. abbrev OAI.NaimarkZFC.PeakingPairData.support line 1119
  122. abbrev OAI.NaimarkZFC.PeakingPairData.start line 1120
  123. theorem OAI.NaimarkZFC.PeakingPairData.core_zero line 1122
  124. def OAI.NaimarkZFC.PeakingPairData.tail line 1129
  125. theorem OAI.NaimarkZFC.PeakingPairData.diagonal_tail line 1133
  126. def OAI.NaimarkZFC.PeakingPairData.matrixPeak line 1141
  127. theorem OAI.NaimarkZFC.PeakingPairData.peak_transfer line 1143
  128. theorem OAI.NaimarkZFC.matrix_eq_sum_entries line 1161
  129. theorem OAI.NaimarkZFC.matrixAux_mem_adjoin line 1169
  130. theorem OAI.NaimarkZFC.matrix_bridge_generators line 1195
  131. abbrev OAI.NaimarkZFC.PeakingPairData.embedBase line 1220
  132. abbrev OAI.NaimarkZFC.PeakingPairData.embedAux line 1221
  133. abbrev OAI.NaimarkZFC.PeakingPairData.modelLetter line 1222
  134. theorem OAI.NaimarkZFC.PeakingPairData.coe_embedBase line 1224
  135. theorem OAI.NaimarkZFC.PeakingPairData.coe_embedAux line 1227
  136. theorem OAI.NaimarkZFC.PeakingPairData.coe_modelLetter line 1230
  137. theorem OAI.NaimarkZFC.PeakingPairData.model_diagonal_agree line 1233
  138. theorem OAI.NaimarkZFC.PeakingPairData.model_factors_dense line 1239
  139. theorem OAI.NaimarkZFC.PeakingPairData.model_words_dense line 1260
  140. theorem OAI.NaimarkZFC.PeakingPairData.coe_core line 1267
  141. theorem OAI.NaimarkZFC.matrixState_isPureState line 1284
  142. theorem OAI.NaimarkZFC.matrix_conjugate_entry line 1311
  143. theorem OAI.NaimarkZFC.matrix_pure_equivalence_reflects line 1317
  144. theorem OAI.NaimarkZFC.state_cross_excision line 1378
  145. theorem OAI.NaimarkZFC.supported_core_decay line 1413
  146. def OAI.NaimarkZFC.bridgeZeroPart line 1440
  147. def OAI.NaimarkZFC.bridgeScalarPart line 1443
  148. theorem OAI.NaimarkZFC.bridge_split line 1446
  149. theorem OAI.NaimarkZFC.bridgeZeroPart_good line 1450
  150. theorem OAI.NaimarkZFC.bridge_four_terms line 1458
  151. structure OAI.NaimarkZFC.BridgeDecayData line 1466
  152. theorem OAI.NaimarkZFC.bridge_left_transfer line 1494
  153. theorem OAI.NaimarkZFC.bridge_right_transfer line 1506
  154. theorem OAI.NaimarkZFC.bridge_left_term line 1518
  155. theorem OAI.NaimarkZFC.bridge_right_term line 1539
  156. theorem OAI.NaimarkZFC.bridge_both_term line 1561
  157. theorem OAI.NaimarkZFC.bridge_word_decay line 1593
  158. abbrev OAI.NaimarkZFC.PeakingPairData.matrixState line 1638
  159. abbrev OAI.NaimarkZFC.PeakingPairData.matrixPeaks line 1639
  160. abbrev OAI.NaimarkZFC.PeakingPairData.matrixPure line 1641
  161. abbrev OAI.NaimarkZFC.PeakingPairData.matrixTrace line 1642
  162. structure OAI.NaimarkZFC.PeakingPairData.Endpoint line 1645
  163. theorem OAI.NaimarkZFC.PeakingPairData.Endpoint.cut line 1664
  164. theorem OAI.NaimarkZFC.PeakingPairData.Endpoint.cut_right line 1683
  165. def OAI.NaimarkZFC.PeakingPairData.Separated line 1703
  166. theorem OAI.NaimarkZFC.PeakingPairData.matrixPeak_trace_null line 1708
  167. def OAI.NaimarkZFC.PeakingPairData.peakEndpoint line 1722
  168. theorem OAI.NaimarkZFC.top_fst line 1742
  169. theorem OAI.NaimarkZFC.top_snd line 1747
  170. theorem OAI.NaimarkZFC.top_pair line 1752
  171. theorem OAI.NaimarkZFC.PeakingPairData.centered_state_zero line 1764
  172. theorem OAI.NaimarkZFC.PeakingPairData.Endpoint.wordData line 1774
  173. theorem OAI.NaimarkZFC.PeakingPairData.Endpoint.word_decay line 1823
  174. theorem OAI.NaimarkZFC.representation_fix_of_coefficient_one line 1842
  175. theorem OAI.NaimarkZFC.representation_coefficient_compression line 1858
  176. theorem OAI.NaimarkZFC.state_two_compression line 1873
  177. theorem OAI.NaimarkZFC.unique_extension_of_dense_word_decay line 1890
  178. theorem OAI.NaimarkZFC.no_common_irrep_of_dense_decay line 1919
  179. theorem OAI.NaimarkZFC.PeakingPairData.Endpoint.model_word_decay line 1951
  180. theorem OAI.NaimarkZFC.PeakingPairData.Endpoint.unique_matrix_extension line 1963
  181. theorem OAI.NaimarkZFC.simple_nonzeroStarHom_injective line 1990
  182. theorem OAI.NaimarkZFC.simple_matrix_corner_injective line 2011
  183. theorem OAI.NaimarkZFC.matrix_pure_corner_ne_zero line 2020
  184. abbrev OAI.NaimarkZFC.PeakingPairData.pureIndex line 2042
  185. instance OAI.NaimarkZFC.PeakingPairData.pureIndexDirected line 2046
  186. def OAI.NaimarkZFC.PeakingPairData.otherEndpoint line 2052
  187. theorem OAI.NaimarkZFC.PeakingPairData.otherEndpoint_value_one line 2087
  188. theorem OAI.NaimarkZFC.matrixSingle_representation_ne_zero line 2107
  189. theorem OAI.NaimarkZFC.PeakingPairData.supported_small_projections line 2123
  190. def OAI.NaimarkZFC.StateExtensionUnique line 2156
  191. theorem OAI.NaimarkZFC.StateExtensionUnique.transport line 2162
  192. theorem OAI.NaimarkZFC.pureState_equivalent_conjugate line 2187
  193. theorem OAI.NaimarkZFC.StateExtensionUnique.of_equivalent line 2206
  194. theorem OAI.NaimarkZFC.pure_extensions_inequivalent_of_no_common line 2224
  195. theorem OAI.NaimarkZFC.PeakingPairData.matrix_unique_of_small line 2260
  196. theorem OAI.NaimarkZFC.PeakingPairData.supported_matrix_unique line 2279
  197. theorem OAI.NaimarkZFC.isState_of_unital_contractive_hermitian line 2292
  198. theorem OAI.NaimarkZFC.cornerCompression_norm line 2320
  199. def OAI.NaimarkZFC.cornerLiftState line 2330
  200. theorem OAI.NaimarkZFC.cornerLiftState_apply line 2334
  201. theorem OAI.NaimarkZFC.cornerLiftState_isState line 2337
  202. theorem OAI.NaimarkZFC.matrixCorner_compression line 2360
  203. theorem OAI.NaimarkZFC.corner_unique_of_matrix line 2369
  204. theorem OAI.NaimarkZFC.exists_state_extension_of_injective line 2392
  205. theorem OAI.NaimarkZFC.StateExtensionUnique.exists_unique_pure line 2414