OAI/Analysis/FreeWords/HaarMoment.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KKWeingarten.matrixPairCLM line 17
  2. theorem OAI.KKWeingarten.matrixPairCLM_apply line 23
  3. theorem OAI.KKWeingarten.positionPair_conjugation line 26
  4. theorem OAI.KKWeingarten.positionPair_average line 46
  5. theorem OAI.KKWeingarten.tensorAverage_gram_formula line 58
  6. def OAI.KKWeingarten.matrixApplyCLM line 76
  7. theorem OAI.KKWeingarten.matrixApplyCLM_apply line 82
  8. theorem OAI.KKWeingarten.tensorAverage_single_apply line 85
  9. theorem OAI.KKWeingarten.matrixPair_single line 102
  10. theorem OAI.KKWeingarten.haar_moment_formula line 107