OAI/Analysis/Naimark/Extension.lean

GitHub source file

87 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.NaimarkZFC.PeakingPairData.state_composite line 22
  2. theorem OAI.NaimarkZFC.PeakingPairData.expectation_composite line 31
  3. theorem OAI.NaimarkZFC.PeakingPairData.turnCentered_of_expectation_zero line 44
  4. theorem OAI.NaimarkZFC.hnnReducedSpan_le_baseTailSpan line 57
  5. theorem OAI.NaimarkZFC.hnnBaseTailSpan_mul_center_span line 63
  6. theorem OAI.NaimarkZFC.hnnBaseTailClosure_mul_center_closure line 79
  7. theorem OAI.NaimarkZFC.hnnBaseTailClosure_expectation_zero line 96
  8. def OAI.NaimarkZFC.hnnAlternatingSpine line 112
  9. theorem OAI.NaimarkZFC.hnnAlternatingSpine_mem_closure line 116
  10. theorem OAI.NaimarkZFC.hnnAlternatingSpine_expectation_zero line 135
  11. def OAI.NaimarkZFC.HNNCenteredBlock line 161
  12. theorem OAI.NaimarkZFC.hnn_alternating_tail_zero line 166
  13. theorem OAI.NaimarkZFC.hnn_alternating_expectation_zero line 206
  14. theorem OAI.NaimarkZFC.hnnReducedSpan_map line 258
  15. theorem OAI.NaimarkZFC.hnnReducedClosure_map line 270
  16. theorem OAI.NaimarkZFC.PeakingPairData.hnn_kernel_reduced line 288
  17. theorem OAI.NaimarkZFC.PeakingPairData.hnnExpectation_state line 295
  18. theorem OAI.NaimarkZFC.PeakingPairData.hnn_mapped_kernel line 308
  19. theorem OAI.NaimarkZFC.PeakingPairData.hnn_free_blocks line 315
  20. theorem OAI.NaimarkZFC.CenteredDecomposition.moments_agree line 336
  21. def OAI.NaimarkZFC.pairedDiagonal line 363
  22. def OAI.NaimarkZFC.pairedFactors line 366
  23. def OAI.NaimarkZFC.pairedCenters line 369
  24. theorem OAI.NaimarkZFC.paired_centered_decomposition line 372
  25. theorem OAI.NaimarkZFC.IsCenteredWord.map_algHom line 413
  26. theorem OAI.NaimarkZFC.wordValue_map_algHom line 423
  27. def OAI.NaimarkZFC.factorCenters line 435
  28. theorem OAI.NaimarkZFC.paired_free_moments_equal line 438
  29. def OAI.NaimarkZFC.jointStarModel line 483
  30. def OAI.NaimarkZFC.jointFirst line 486
  31. def OAI.NaimarkZFC.jointSecond line 489
  32. theorem OAI.NaimarkZFC.jointFirst_dense line 493
  33. theorem OAI.NaimarkZFC.jointSecond_dense line 505
  34. theorem OAI.NaimarkZFC.jointStarModel_moments line 531
  35. def OAI.NaimarkZFC.jointFreeEquiv line 547
  36. theorem OAI.NaimarkZFC.jointFreeEquiv_factor line 561
  37. theorem OAI.NaimarkZFC.jointFreeEquiv_preserves line 570
  38. theorem OAI.NaimarkZFC.wordValue_reindex line 581
  39. theorem OAI.NaimarkZFC.PeakingPairData.hnn_family_free line 601
  40. theorem OAI.NaimarkZFC.PeakingPairData.hnn_two_factors_dense line 618
  41. def OAI.NaimarkZFC.PeakingPairData.pairHNN line 640
  42. instance OAI.NaimarkZFC.PeakingPairData.pairHNN_cstar line 641
  43. def OAI.NaimarkZFC.PeakingPairData.pairHNNBase line 644
  44. def OAI.NaimarkZFC.PeakingPairData.pairHNNExpect line 648
  45. theorem OAI.NaimarkZFC.PeakingPairData.pairHNNExpect_fix line 652
  46. theorem OAI.NaimarkZFC.PeakingPairData.pairHNNExpect_left line 658
  47. def OAI.NaimarkZFC.PeakingPairData.leftHNNFamily line 667
  48. def OAI.NaimarkZFC.PeakingPairData.rightHNNFamily line 671
  49. theorem OAI.NaimarkZFC.PeakingPairData.leftHNNFamily_base line 675
  50. theorem OAI.NaimarkZFC.PeakingPairData.rightHNNFamily_base line 682
  51. theorem OAI.NaimarkZFC.PeakingPairData.leftHNNFamily_free line 689
  52. theorem OAI.NaimarkZFC.PeakingPairData.rightHNNFamily_free line 706
  53. theorem OAI.NaimarkZFC.PeakingPairData.leftHNNFamily_dense line 723
  54. theorem OAI.NaimarkZFC.PeakingPairData.rightHNNFamily_dense line 729
  55. theorem OAI.NaimarkZFC.PeakingPairData.reorder_base_moments line 746
  56. def OAI.NaimarkZFC.PeakingPairData.reorderEquiv line 750
  57. theorem OAI.NaimarkZFC.PeakingPairData.reorderEquiv_factor line 763
  58. theorem OAI.NaimarkZFC.PeakingPairData.reorderEquiv_trace line 778
  59. theorem OAI.NaimarkZFC.PeakingPairData.hnn_reorder_of_peaks line 802
  60. theorem OAI.NaimarkZFC.PeakingPairData.hnn_reorder line 825
  61. theorem OAI.NaimarkZFC.PeakingPairData.omitted_pair_classes_excluded line 851
  62. theorem OAI.NaimarkZFC.PeakingPairData.hnn_preserves_omitted_pair line 869
  63. theorem OAI.NaimarkZFC.PeakingPairData.separated_of_inequivalent line 906
  64. theorem OAI.NaimarkZFC.PeakingPairData.hnnPush_separated line 918
  65. theorem OAI.NaimarkZFC.PeakingPairData.reordered_inclusion_pureUEP line 937
  66. theorem OAI.NaimarkZFC.exists_bounded_selfAdjoint_operator_vector line 972
  67. theorem OAI.NaimarkZFC.neg_saCayley_sub_one_norm line 1023
  68. theorem OAI.NaimarkZFC.irreducible_near_unitary_vector line 1041
  69. def OAI.NaimarkZFC.directLimitFunctional line 1102
  70. theorem OAI.NaimarkZFC.directLimitFunctional_stage line 1110
  71. def OAI.NaimarkZFC.cstarDirectLimitState line 1113
  72. theorem OAI.NaimarkZFC.cstarDirectLimitState_stage line 1116
  73. theorem OAI.NaimarkZFC.cstarDirectLimitState_isState line 1120
  74. theorem OAI.NaimarkZFC.cstarDirectLimitState_tracial line 1142
  75. theorem OAI.NaimarkZFC.tracial_gns_zero_of_square_zero line 1162
  76. theorem OAI.NaimarkZFC.tracialState_strictPos_of_simple line 1177
  77. theorem OAI.NaimarkZFC.cstarDirectLimit_simple line 1213
  78. theorem OAI.NaimarkZFC.cstarDirectLimitState_strictPos line 1220
  79. theorem OAI.NaimarkZFC.cstarDirectLimitInclude_tail_dense line 1232
  80. theorem OAI.NaimarkZFC.cstarDirectLimit_pureUEP line 1241
  81. theorem OAI.NaimarkZFC.PeakingPairData.pulled_peaks line 1266
  82. def OAI.NaimarkZFC.PeakingPairData.pullback line 1269
  83. theorem OAI.NaimarkZFC.PeakingPairData.pullback_unique line 1293
  84. theorem OAI.NaimarkZFC.PeakingPairData.pullback_separated line 1297
  85. theorem OAI.NaimarkZFC.PeakingPairData.pullback_hnn_inclusion line 1317
  86. instance OAI.NaimarkZFC.hnnGeneratedCStar line 1330
  87. theorem OAI.NaimarkZFC.PeakingPairData.hnn_generated_step line 1342