OAI/Analysis/Naimark/States.lean

GitHub source file

106 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.NaimarkZFC.cornerSubalgebra line 11
  2. instance OAI.NaimarkZFC.cornerClosed line 29
  3. abbrev OAI.NaimarkZFC.CStarCorner line 33
  4. instance OAI.NaimarkZFC.cornerOne line 35
  5. theorem OAI.NaimarkZFC.corner_coe_one line 38
  6. instance OAI.NaimarkZFC.cornerRing line 40
  7. instance OAI.NaimarkZFC.cornerNormedRing line 56
  8. instance OAI.NaimarkZFC.cornerAlgebra line 59
  9. instance OAI.NaimarkZFC.cornerCStarAlgebra line 62
  10. instance OAI.NaimarkZFC.cornerPartialOrder line 66
  11. instance OAI.NaimarkZFC.cornerStarOrderedRing line 69
  12. def OAI.NaimarkZFC.cornerCompression line 72
  13. theorem OAI.NaimarkZFC.cornerCompression_coe line 87
  14. theorem OAI.NaimarkZFC.cornerCompression_corner line 90
  15. def OAI.NaimarkZFC.weakStates line 100
  16. theorem OAI.NaimarkZFC.isClosed_weakStates line 103
  17. theorem OAI.NaimarkZFC.isCompact_weakStates line 114
  18. theorem OAI.NaimarkZFC.state_eq_one_of_projection_le line 122
  19. theorem OAI.NaimarkZFC.Peaks.tendsto_supported line 133
  20. theorem OAI.NaimarkZFC.Peaks.tendsto_supported_apply line 148
  21. def OAI.NaimarkZFC.cornerFunctional line 155
  22. theorem OAI.NaimarkZFC.cornerFunctional_apply line 159
  23. def OAI.NaimarkZFC.cornerState line 162
  24. theorem OAI.NaimarkZFC.cornerState_apply line 166
  25. theorem OAI.NaimarkZFC.state_projection_real line 170
  26. theorem OAI.NaimarkZFC.cornerState_isState line 177
  27. theorem OAI.NaimarkZFC.cornerState_eq_one line 193
  28. def OAI.NaimarkZFC.peakAtom line 201
  29. theorem OAI.NaimarkZFC.Peaks.peakAtom_projection line 203
  30. theorem OAI.NaimarkZFC.Peaks.peakAtom_le line 207
  31. theorem OAI.NaimarkZFC.Peaks.tendsto_atomState line 211
  32. theorem OAI.NaimarkZFC.selfAdjoint_nonneg_of_norm_one line 224
  33. def OAI.NaimarkZFC.selfAdjointComplexify line 243
  34. theorem OAI.NaimarkZFC.selfAdjointComplexify_coe line 252
  35. def OAI.NaimarkZFC.selfAdjointPositive line 256
  36. theorem OAI.NaimarkZFC.selfAdjointPositive_coe line 264
  37. theorem OAI.NaimarkZFC.selfAdjointPositive_one line 269
  38. def OAI.NaimarkZFC.selfAdjointSubspace line 273
  39. def OAI.NaimarkZFC.selfAdjointSubspaceInclusion line 276
  40. theorem OAI.NaimarkZFC.exists_state_extension_subalgebra line 285
  41. theorem OAI.NaimarkZFC.character_isState line 351
  42. theorem OAI.NaimarkZFC.exists_norming_state line 364
  43. theorem OAI.NaimarkZFC.orthogonalProjection_commute line 389
  44. theorem OAI.NaimarkZFC.normal_orthogonalProjection_sum line 395
  45. theorem OAI.NaimarkZFC.norm_orthogonalProjection_sum_le line 407
  46. theorem OAI.NaimarkZFC.summable_orthogonalProjection line 437
  47. theorem OAI.NaimarkZFC.orthogonalProjection_mul_tsum line 454
  48. theorem OAI.NaimarkZFC.norm_orthogonalProjection_tsum_le line 464
  49. theorem OAI.NaimarkZFC.Peaks.peakAtom_mul_peak line 474
  50. theorem OAI.NaimarkZFC.Peaks.peak_mul_peakAtom line 480
  51. theorem OAI.NaimarkZFC.Peaks.peakAtom_orthogonal line 486
  52. theorem OAI.NaimarkZFC.peakAtom_sum line 499
  53. def OAI.NaimarkZFC.peakDiagonal line 505
  54. theorem OAI.NaimarkZFC.peakDiagonal_partial line 510
  55. theorem OAI.NaimarkZFC.Peaks.norm_peakDiagonal_partial_le line 518
  56. theorem OAI.NaimarkZFC.Peaks.tendsto_peakDiagonal line 549
  57. theorem OAI.NaimarkZFC.Peaks.norm_peakDiagonal_le line 557
  58. theorem OAI.NaimarkZFC.Peaks.summable_expectationTail line 566
  59. def OAI.NaimarkZFC.peakingExpectationFun line 572
  60. theorem OAI.NaimarkZFC.Peaks.peakingExpectationFun_add line 575
  61. theorem OAI.NaimarkZFC.peakingExpectationFun_smul line 592
  62. theorem OAI.NaimarkZFC.Peaks.norm_peakingExpectationFun_le line 598
  63. def OAI.NaimarkZFC.peakingExpectation line 607
  64. theorem OAI.NaimarkZFC.peakingExpectation_apply line 618
  65. theorem OAI.NaimarkZFC.peakingExpectation_one line 623
  66. theorem OAI.NaimarkZFC.peakingExpectation_nonneg line 633
  67. theorem OAI.NaimarkZFC.cornerFunctional_norm_apply_le line 652
  68. theorem OAI.NaimarkZFC.trace_compression line 668
  69. theorem OAI.NaimarkZFC.trace_cornerState_smul line 674
  70. theorem OAI.NaimarkZFC.trace_peaking_partial line 683
  71. theorem OAI.NaimarkZFC.trace_peak_mul_tendsto_zero line 697
  72. theorem OAI.NaimarkZFC.peakingExpectation_trace line 708
  73. theorem OAI.NaimarkZFC.peakingExpectation_faithful line 725
  74. theorem OAI.NaimarkZFC.Peaks.mul_peak line 737
  75. def OAI.NaimarkZFC.peakSpanAlgebra line 745
  76. def OAI.NaimarkZFC.peakAlgebra line 783
  77. theorem OAI.NaimarkZFC.peak_mem_peakAlgebra line 787
  78. theorem OAI.NaimarkZFC.peakAtom_mem_peakAlgebra line 791
  79. theorem OAI.NaimarkZFC.peakAlgebra_eq_spanClosure line 794
  80. theorem OAI.NaimarkZFC.peakingExpectation_mem line 809
  81. theorem OAI.NaimarkZFC.Peaks.apply_peakAtom line 827
  82. theorem OAI.NaimarkZFC.cornerState_peakAtom_of_ne line 831
  83. theorem OAI.NaimarkZFC.peakingExpectation_peakAtom line 836
  84. theorem OAI.NaimarkZFC.peakingExpectation_peak line 848
  85. theorem OAI.NaimarkZFC.peakingExpectation_fixes line 862
  86. theorem OAI.NaimarkZFC.mul_idempotent_compression line 888
  87. theorem OAI.NaimarkZFC.Peaks.apply_peakAtom_mul line 895
  88. theorem OAI.NaimarkZFC.peakingExpectation_peakAtom_mul line 904
  89. theorem OAI.NaimarkZFC.peakAtom_mul_peakingExpectation line 919
  90. theorem OAI.NaimarkZFC.positiveFunctional_matrix_square_nonneg line 946
  91. theorem OAI.NaimarkZFC.positiveFunctional_matrix_nonneg line 983
  92. def OAI.NaimarkZFC.positiveFunctionalCP line 997
  93. def OAI.NaimarkZFC.projectionScalarHom line 1006
  94. def OAI.NaimarkZFC.projectionFunctionalCP line 1016
  95. theorem OAI.NaimarkZFC.peaking_partial_matrix_nonneg line 1023
  96. def OAI.NaimarkZFC.peakingExpectationCP line 1043
  97. theorem OAI.NaimarkZFC.peakingExpectation_peak_mul line 1066
  98. theorem OAI.NaimarkZFC.peakingExpectation_leftBimodule line 1079
  99. theorem OAI.NaimarkZFC.peakingExpectation_star line 1103
  100. theorem OAI.NaimarkZFC.peakingExpectation_rightBimodule line 1110
  101. theorem OAI.NaimarkZFC.peakingExpectation_idempotent line 1120
  102. theorem OAI.NaimarkZFC.nontrivial_of_state line 1131
  103. theorem OAI.NaimarkZFC.state_corner_bound line 1138
  104. theorem OAI.NaimarkZFC.exists_supported_norming_state line 1152
  105. theorem OAI.NaimarkZFC.Peaks.excision_selfAdjoint line 1184
  106. theorem OAI.NaimarkZFC.Peaks.excision line 1200