OAI/Analysis/Laughlin/Spin/Haar.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.Laughlin.Rotation.sourceSU2_measurableSpace line 10
  2. instance OAI.Laughlin.Rotation.sourceSU2_borelSpace line 11
  3. def OAI.Laughlin.Rotation.sourceHaar line 13
  4. instance OAI.Laughlin.Rotation.sourceHaar_isHaar line 16
  5. instance OAI.Laughlin.Rotation.sourceHaar_isProbability line 19
  6. theorem OAI.Laughlin.Rotation.sourceHaar_univ line 23
  7. theorem OAI.Laughlin.Rotation.source_tensor_haar_average_commutes line 25
  8. theorem OAI.Laughlin.Rotation.source_tensor_haar_average_trace line 32