OAI/Analysis/Naimark/Basic.lean

GitHub source file

136 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.NaimarkZFC.IsSimpleCStar line 11

    Also declared: ComparatorChallenges/Naimark.lean:11 (same declaration text).

  2. def OAI.NaimarkZFC.IsState line 14

    Also declared: ComparatorChallenges/Naimark.lean:14 (same declaration text).

  3. def OAI.NaimarkZFC.IsFaithfulTracialState line 17

    Also declared: ComparatorChallenges/Naimark.lean:17 (same declaration text).

  4. def OAI.NaimarkZFC.IsIrreducible line 21

    Also declared: ComparatorChallenges/Naimark.lean:21 (same declaration text).

  5. def OAI.NaimarkZFC.UnitarilyEquivalent line 27

    Also declared: ComparatorChallenges/Naimark.lean:27 (same declaration text).

  6. def OAI.NaimarkZFC.HasUniqueIrreducibleRepresentation line 33

    Also declared: ComparatorChallenges/Naimark.lean:33 (same declaration text).

  7. def OAI.NaimarkZFC.IsIsomorphicToCompacts line 39

    Also declared: ComparatorChallenges/Naimark.lean:39 (same declaration text).

  8. inductive OAI.NaimarkZFC.HNNWord line 46
  9. def OAI.NaimarkZFC.HNNWord.first line 52
  10. def OAI.NaimarkZFC.HNNWord.eval line 56
  11. def OAI.NaimarkZFC.HNNWord.Reduced line 60
  12. def OAI.NaimarkZFC.hnnWordSet line 68
  13. def OAI.NaimarkZFC.hnnWordSpan line 71
  14. theorem OAI.NaimarkZFC.hnnWordSpan_base line 73
  15. theorem OAI.NaimarkZFC.hnnWordSpan_word line 76
  16. theorem OAI.NaimarkZFC.hnnWordSpan_letter line 80
  17. theorem OAI.NaimarkZFC.hnnWordSpan_mul_base line 84
  18. theorem OAI.NaimarkZFC.hnnWordSpan_left_word line 100
  19. theorem OAI.NaimarkZFC.hnnWordSpan_mul_letter line 133
  20. theorem OAI.NaimarkZFC.adjoin_le_hnnWordSpan line 145
  21. def OAI.NaimarkZFC.gnsVector line 179
  22. theorem OAI.NaimarkZFC.gns_apply_coe line 181
  23. theorem OAI.NaimarkZFC.gns_apply_vector line 186
  24. theorem OAI.NaimarkZFC.gnsVector_cyclic line 190
  25. theorem OAI.NaimarkZFC.gnsVector_coefficient line 195
  26. theorem OAI.NaimarkZFC.gnsVector_norm_sq line 199
  27. theorem OAI.NaimarkZFC.positive_norm_apply_le line 206
  28. def OAI.NaimarkZFC.positiveCLM line 220
  29. theorem OAI.NaimarkZFC.positiveCLM_apply line 223
  30. theorem OAI.NaimarkZFC.positiveCLM_norm line 225
  31. def OAI.NaimarkZFC.positiveOfSquares line 238
  32. theorem OAI.NaimarkZFC.positiveOfSquares_apply line 249
  33. theorem OAI.NaimarkZFC.positiveCLM_positiveOfSquares line 253
  34. theorem OAI.NaimarkZFC.isState_iff line 257
  35. theorem OAI.NaimarkZFC.gnsVector_norm_eq_one line 274
  36. theorem OAI.NaimarkZFC.gns_fix_of_value_one line 279
  37. theorem OAI.NaimarkZFC.positive_compression line 299
  38. theorem OAI.NaimarkZFC.state_map_star line 315
  39. theorem OAI.NaimarkZFC.state_norm_apply_le line 320
  40. theorem OAI.NaimarkZFC.state_compression line 323
  41. def OAI.NaimarkZFC.IsPureState line 328
  42. theorem OAI.NaimarkZFC.convex_states line 331
  43. theorem OAI.NaimarkZFC.state_projection_face line 345
  44. def OAI.NaimarkZFC.Peaks line 363
  45. theorem OAI.NaimarkZFC.Peaks.isPureState line 370
  46. theorem OAI.NaimarkZFC.state_nonneg line 384
  47. theorem OAI.NaimarkZFC.state_contraction_face line 387
  48. theorem OAI.NaimarkZFC.state_excision_error line 403
  49. theorem OAI.NaimarkZFC.pure_of_dense_excision line 413
  50. def OAI.NaimarkZFC.starAlgHomCLM line 447
  51. theorem OAI.NaimarkZFC.starAlgHomCLM_apply line 453
  52. def OAI.NaimarkZFC.restrictState line 456
  53. theorem OAI.NaimarkZFC.restrictState_apply line 460
  54. theorem OAI.NaimarkZFC.isState_restrict line 463
  55. theorem OAI.NaimarkZFC.restrictState_convex line 473
  56. theorem OAI.NaimarkZFC.unique_lift_pure line 478
  57. theorem OAI.NaimarkZFC.irreducible_map_one line 496
  58. def OAI.NaimarkZFC.orbitMap line 518
  59. theorem OAI.NaimarkZFC.orbitMap_apply line 523
  60. theorem OAI.NaimarkZFC.irreducible_vector_cyclic line 526
  61. def OAI.NaimarkZFC.orbitCLM line 548
  62. def OAI.NaimarkZFC.vectorFunctional line 555
  63. theorem OAI.NaimarkZFC.vectorFunctional_apply line 558
  64. theorem OAI.NaimarkZFC.vectorFunctional_square line 561
  65. theorem OAI.NaimarkZFC.vectorFunctional_one line 567
  66. theorem OAI.NaimarkZFC.vectorFunctional_norm_le line 571
  67. theorem OAI.NaimarkZFC.isState_vectorFunctional line 582
  68. theorem OAI.NaimarkZFC.irreducible_vector_state line 599
  69. theorem OAI.NaimarkZFC.invariant_orthogonal line 603
  70. theorem OAI.NaimarkZFC.invariant_starProjection_commute line 611
  71. theorem OAI.NaimarkZFC.vectorFunctional_add_reducing line 620
  72. theorem OAI.NaimarkZFC.normalized_vector_isState line 635
  73. theorem OAI.NaimarkZFC.cyclic_closed_invariant_top line 652
  74. theorem OAI.NaimarkZFC.pure_cyclic_irreducible line 662
  75. theorem OAI.NaimarkZFC.pure_gns_irreducible line 737
  76. theorem OAI.NaimarkZFC.irreducible_commutant_denseRange line 752
  77. theorem OAI.NaimarkZFC.commutant_mul_eq_zero line 776
  78. theorem OAI.NaimarkZFC.irreducible_commutant_selfAdjoint_scalar line 789
  79. def OAI.NaimarkZFC.dominatedPreGNS line 837
  80. theorem OAI.NaimarkZFC.dominatedPreGNS_apply line 846
  81. def OAI.NaimarkZFC.dominatedGNS line 850
  82. theorem OAI.NaimarkZFC.dominatedGNS_apply_coe line 854
  83. theorem OAI.NaimarkZFC.dominatedGNS_apply_vector line 859
  84. theorem OAI.NaimarkZFC.dominatedGNS_intertwines line 864
  85. theorem OAI.NaimarkZFC.intertwiner_adjoint_comp_commute line 879
  86. theorem OAI.NaimarkZFC.positive_eq_smul_of_gns_irreducible line 892
  87. theorem OAI.NaimarkZFC.isPureState_of_gns_irreducible line 921
  88. theorem OAI.NaimarkZFC.isPureState_iff_gns_irreducible line 950
  89. def OAI.NaimarkZFC.cyclicPreGNS line 957
  90. theorem OAI.NaimarkZFC.cyclicPreGNS_apply line 970
  91. def OAI.NaimarkZFC.cyclicGNSMap line 975
  92. theorem OAI.NaimarkZFC.cyclicGNSMap_apply line 979
  93. theorem OAI.NaimarkZFC.cyclicGNSMap_norm line 985
  94. def OAI.NaimarkZFC.cyclicGNSIsometry line 997
  95. theorem OAI.NaimarkZFC.cyclicGNSIsometry_surjective line 1002
  96. def OAI.NaimarkZFC.cyclicGNSEquiv line 1017
  97. theorem OAI.NaimarkZFC.cyclicGNSEquiv_intertwines line 1023
  98. theorem OAI.NaimarkZFC.faithful_gns_injective line 1049
  99. def OAI.NaimarkZFC.gnsOrbit line 1058
  100. theorem OAI.NaimarkZFC.gnsOrbit_apply line 1072
  101. theorem OAI.NaimarkZFC.gnsOrbit_dense line 1075
  102. theorem OAI.NaimarkZFC.gnsOrbit_norm line 1078
  103. def OAI.NaimarkZFC.momentGNSEquiv line 1089
  104. theorem OAI.NaimarkZFC.momentGNSEquiv_apply line 1099
  105. theorem OAI.NaimarkZFC.momentGNSEquiv_intertwines line 1103
  106. theorem OAI.NaimarkZFC.norm_eq_of_faithful_moments line 1125
  107. def OAI.NaimarkZFC.starAlgEquivOfDenseNorm line 1150
  108. theorem OAI.NaimarkZFC.starAlgEquivOfDenseNorm_apply line 1177
  109. def OAI.NaimarkZFC.starAlgEquivOfFaithfulMoments line 1183
  110. theorem OAI.NaimarkZFC.starAlgEquivOfFaithfulMoments_apply line 1191
  111. theorem OAI.NaimarkZFC.starAlgEquivOfFaithfulMoments_preserves line 1199
  112. theorem OAI.NaimarkZFC.hnn_generators_star line 1220
  113. theorem OAI.NaimarkZFC.hnn_moments_equal line 1231
  114. theorem OAI.NaimarkZFC.hnn_pair_fst_dense line 1280
  115. theorem OAI.NaimarkZFC.hnn_pair_snd_dense line 1295
  116. def OAI.NaimarkZFC.hnnFaithfulEquiv line 1326
  117. theorem OAI.NaimarkZFC.hnnFaithfulEquiv_base line 1336
  118. theorem OAI.NaimarkZFC.hnnFaithfulEquiv_letter line 1345
  119. theorem OAI.NaimarkZFC.hnnFaithfulEquiv_preserves line 1354
  120. def OAI.NaimarkZFC.hnnGenerated line 1366
  121. theorem OAI.NaimarkZFC.hnnGenerated_isClosed line 1369
  122. def OAI.NaimarkZFC.hnnGeneratedBase line 1373
  123. def OAI.NaimarkZFC.hnnGeneratedLetter line 1376
  124. theorem OAI.NaimarkZFC.hnnGenerated_dense line 1379
  125. def OAI.NaimarkZFC.restrictPositive line 1412
  126. theorem OAI.NaimarkZFC.restrictPositive_apply line 1422
  127. theorem OAI.NaimarkZFC.restrictPositive_faithful line 1426
  128. theorem OAI.NaimarkZFC.exists_hnnRestriction line 1435
  129. def OAI.NaimarkZFC.hnnReducedSpan line 1502
  130. theorem OAI.NaimarkZFC.hnnWordSpan_center_mem line 1505
  131. theorem OAI.NaimarkZFC.hnnWordSpan_dense line 1520
  132. theorem OAI.NaimarkZFC.hnn_kernel_mem_closure_reducedSpan line 1537
  133. theorem OAI.NaimarkZFC.hnn_starAdjoin_le_wordSpan line 1559
  134. theorem OAI.NaimarkZFC.expectation_mem_smaller_base line 1575
  135. theorem OAI.NaimarkZFC.HNNWord.eval_hom line 1601
  136. theorem OAI.NaimarkZFC.hnn_expectation_intertwines line 1609