OAI/Analysis/FreeGroupFactor/Operators.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FreeGroupFactorMain.hilbertReindex line 16
  2. theorem OAI.FreeGroupFactorMain.hilbertReindex_apply line 35
  3. def OAI.FreeGroupFactorMain.leftRegular line 38
  4. theorem OAI.FreeGroupFactorMain.leftRegular_apply line 41
  5. theorem OAI.FreeGroupFactorMain.leftRegular_one line 44
  6. theorem OAI.FreeGroupFactorMain.leftRegular_mul line 49
  7. theorem OAI.FreeGroupFactorMain.leftRegular_mem_leftTranslations line 54
  8. theorem OAI.FreeGroupFactorMain.leftTranslations_eq_range line 57
  9. def OAI.FreeGroupFactorMain.groupVonNeumannBundled line 68
  10. theorem OAI.FreeGroupFactorMain.leftRegular_star line 76
  11. def OAI.FreeGroupFactorMain.rightRegular line 84
  12. theorem OAI.FreeGroupFactorMain.rightRegular_apply line 87
  13. theorem OAI.FreeGroupFactorMain.rightRegular_star line 91
  14. theorem OAI.FreeGroupFactorMain.left_right_commute line 99
  15. theorem OAI.FreeGroupFactorMain.rightRegular_mem_commutant line 104
  16. theorem OAI.FreeGroupFactorMain.groupVN_commute_right line 110
  17. theorem OAI.FreeGroupFactorMain.groupVN_separating line 114
  18. theorem OAI.FreeGroupFactorMain.canonicalTrace_eq_inner line 137
  19. theorem OAI.FreeGroupFactorMain.canonicalTrace_star_mul line 147
  20. theorem OAI.FreeGroupFactorMain.canonicalTrace_faithful line 157
  21. def OAI.FreeGroupFactorMain.canonicalTraceLinear line 164
  22. theorem OAI.FreeGroupFactorMain.norm_canonicalTrace_le line 169
  23. def OAI.FreeGroupFactorMain.canonicalTraceCLM line 184
  24. theorem OAI.FreeGroupFactorMain.canonicalTraceCLM_apply line 189
  25. theorem OAI.FreeGroupFactorMain.leftRegular_unitary line 192
  26. theorem OAI.FreeGroupFactorMain.leftRegular_mem_groupVN line 197
  27. def OAI.FreeGroupFactorMain.groupUnitary line 207
  28. theorem OAI.FreeGroupFactorMain.canonicalTrace_groupUnitary line 210