OAI/Analysis/FactorGeneration/Bicommutant.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Finite diagonal amplification and the projection onto a simultaneous operator orbit. These are the analytic ingredients of the bicommutant theorem.

  1. abbrev OAI.Generator.FiniteHilbert line 24
  2. def OAI.Generator.diagonalOperator line 26
  3. theorem OAI.Generator.diagonalOperator_apply line 31
  4. theorem OAI.Generator.diagonalOperator_star line 34
  5. def OAI.Generator.tupleOrbitMap line 44
  6. def OAI.Generator.tupleOrbitClosure line 50
  7. instance OAI.Generator.tupleOrbitClosure_complete line 53
  8. theorem OAI.Generator.mem_tupleOrbitClosure line 57
  9. theorem OAI.Generator.tupleOrbitClosure_invariant line 64
  10. theorem OAI.Generator.starProjection_commutes_of_invariant line 78
  11. theorem OAI.Generator.tupleOrbitProjection_commutes line 90
  12. def OAI.Generator.tupleSingle line 101
  13. theorem OAI.Generator.tupleSingle_apply line 106
  14. theorem OAI.Generator.tuple_eq_sum_single line 110
  15. theorem OAI.Generator.diagonalOperator_single line 116
  16. def OAI.Generator.operatorEntry line 121
  17. theorem OAI.Generator.operatorEntry_mem_centralizer line 125
  18. theorem OAI.Generator.diagonalOperator_commutes_of_entries line 138
  19. theorem OAI.Generator.bicommutant_tuple_mem_closure line 150
  20. theorem OAI.Generator.bicommutant_finite_strong_approximation line 173
  21. theorem OAI.Generator.bicommutant_exists_strong_net line 186
  22. theorem OAI.Generator.wotClosed_bicommutant line 206
  23. def OAI.Generator.vonNeumannOfWOTClosed line 221
  24. theorem OAI.Generator.wotClosed_normClosed line 226
  25. theorem OAI.Generator.countable_monoid_closure line 236
  26. theorem OAI.Generator.separable_countable_star_adjoin line 243