OAI/Analysis/FreeWords/TensorHaar.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.KKWeingarten.matrixUnitaryMeasurable line 16
  2. instance OAI.KKWeingarten.matrixUnitaryBorel line 18
  3. instance OAI.KKWeingarten.matrixUnitaryCompact line 20
  4. def OAI.KKWeingarten.matrixHaar line 30
  5. instance OAI.KKWeingarten.matrixHaar_probability line 33
  6. instance OAI.KKWeingarten.matrixHaar_leftInvariant line 37
  7. theorem OAI.KKWeingarten.tensorMatrix_mul line 41
  8. theorem OAI.KKWeingarten.tensorMatrix_one line 51
  9. theorem OAI.KKWeingarten.tensorMatrix_star line 59
  10. theorem OAI.KKWeingarten.tensorMatrix_unitary line 64
  11. theorem OAI.KKWeingarten.continuous_tensorMatrix line 70
  12. def OAI.KKWeingarten.tensorAverage line 75
  13. theorem OAI.KKWeingarten.continuous_tensorConjugation line 80
  14. theorem OAI.KKWeingarten.tensorAverage_commute line 88
  15. theorem OAI.KKWeingarten.tensorAverage_span line 126