OAI/Analysis/LaughlinFock/Averaging.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Averaging.

  1. def OAI.LaughlinFock.rotationHaar line 27
  2. instance OAI.LaughlinFock.rotationHaar_probability line 30
  3. instance OAI.LaughlinFock.rotationHaar_leftInvariant line 33
  4. def OAI.LaughlinFock.rotationEvaluation line 37
  5. theorem OAI.LaughlinFock.rotationEvaluation_continuous line 42
  6. theorem OAI.LaughlinFock.rotationEvaluation_unitary line 46
  7. theorem OAI.LaughlinFock.rotationOrbit_integrable line 52
  8. def OAI.LaughlinFock.rotationAverage line 62
  9. theorem OAI.LaughlinFock.rotationAverage_posSemidef line 65
  10. theorem OAI.LaughlinFock.rotationAverage_trace line 69
  11. theorem OAI.LaughlinFock.rotationAverage_commutes line 74
  12. theorem OAI.LaughlinFock.rotationAverage_covariance line 83
  13. theorem OAI.LaughlinFock.rotationAverage_one line 94
  14. theorem OAI.LaughlinFock.rotationAverage_add line 101
  15. theorem OAI.LaughlinFock.rotationAverage_smul line 106
  16. def OAI.LaughlinFock.rotationAverageLinear line 112
  17. theorem OAI.LaughlinFock.rotationAverage_real_smul line 117
  18. theorem OAI.LaughlinFock.rotationAverage_relative line 121