OAI/Analysis/RotationWeights/TracialAction.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ContinuousCircleWeight.rightTranslate line 20
  2. lemma OAI.ContinuousCircleWeight.rightTranslate_apply line 23
  3. def OAI.ContinuousCircleWeight.rightOperator line 29
  4. lemma OAI.ContinuousCircleWeight.rightOperator_vacuum line 32
  5. lemma OAI.ContinuousCircleWeight.rightOperator_U line 46
  6. lemma OAI.ContinuousCircleWeight.rightOperator_V line 56
  7. def OAI.ContinuousCircleWeight.regularAlgebra line 68
  8. lemma OAI.ContinuousCircleWeight.in_regularAlgebra_commutes line 71
  9. lemma OAI.ContinuousCircleWeight.regular_column line 81
  10. lemma OAI.ContinuousCircleWeight.regular_adjoint_coefficient line 86
  11. lemma OAI.ContinuousCircleWeight.regular_adjoint_norm_vacuum line 99
  12. lemma OAI.ContinuousCircleWeight.regular_vacuum_separating line 111
  13. def OAI.ContinuousCircleWeight.fiberConjugacy line 131
  14. lemma OAI.ContinuousCircleWeight.fiberConjugacy_apply line 133
  15. lemma OAI.ContinuousCircleWeight.fiberConjugacy_U line 137
  16. lemma OAI.ContinuousCircleWeight.fiberConjugacy_V line 138
  17. def OAI.ContinuousCircleWeight.regularCommutant line 140
  18. def OAI.ContinuousCircleWeight.fiberCommutant line 142
  19. lemma OAI.ContinuousCircleWeight.commute_star_unitary line 145
  20. lemma OAI.ContinuousCircleWeight.mem_regularCommutant line 153
  21. lemma OAI.ContinuousCircleWeight.regularAlgebra_of_commutes line 163
  22. lemma OAI.ContinuousCircleWeight.fiber_commutes_of_regularAlgebra line 172
  23. lemma OAI.ContinuousCircleWeight.realPi_fiberCommutant line 181
  24. def OAI.ContinuousCircleWeight.fiberVacuum line 202
  25. lemma OAI.ContinuousCircleWeight.fiber_vacuum_trace line 203
  26. lemma OAI.ContinuousCircleWeight.fiber_vacuum_faithful line 215