OAI/Analysis/FreeWords/Bicommutant.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniversalStrongKK.DirectSum line 18
  2. def OAI.UniversalStrongKK.diagonalOp line 21
  3. theorem OAI.UniversalStrongKK.diagonalOp_apply line 26
  4. theorem OAI.UniversalStrongKK.diagonalOp_star line 29
  5. def OAI.UniversalStrongKK.coordinateOp line 40
  6. theorem OAI.UniversalStrongKK.coordinateOp_apply line 46
  7. theorem OAI.UniversalStrongKK.diagonalOp_single line 52
  8. theorem OAI.UniversalStrongKK.coordinate_commute_of_diagonal line 60
  9. theorem OAI.UniversalStrongKK.sum_single_direct line 71
  10. theorem OAI.UniversalStrongKK.diagonal_commute_of_coordinates line 77
  11. theorem OAI.UniversalStrongKK.commute_projection_of_invariant line 91
  12. def OAI.UniversalStrongKK.orbitCore line 107
  13. def OAI.UniversalStrongKK.closedOrbit line 122
  14. instance OAI.UniversalStrongKK.closedOrbit_complete line 125
  15. theorem OAI.UniversalStrongKK.diagonal_closedOrbit_mem line 129
  16. theorem OAI.UniversalStrongKK.identityVector_mem_closedOrbit line 139
  17. theorem OAI.UniversalStrongKK.bicommutant_diagonal_mem_closedOrbit line 145
  18. theorem OAI.UniversalStrongKK.bicommutant_strong_approximation line 170