OAI/Probability/SignedSweeps/TensorCommutant.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SignedSweeps.span_monomial_evaluations line 10
  2. def OAI.SignedSweeps.wordHistogram line 35
  3. lemma OAI.SignedSweeps.wordHistogram_apply line 38
  4. lemma OAI.SignedSweeps.wordHistogram_le line 42
  5. lemma OAI.SignedSweeps.wordHistogram_relabel line 47
  6. lemma OAI.SignedSweeps.wordHistogram_eq_orbit line 51
  7. lemma OAI.SignedSweeps.wordHistogram_monomial_eval line 61
  8. def OAI.SignedSweeps.wordPairHistogram line 68
  9. abbrev OAI.SignedSweeps.WordOrbit line 71
  10. instance OAI.SignedSweeps.wordOrbitFinite line 74
  11. instance OAI.SignedSweeps.wordOrbitFintype line 81
  12. lemma OAI.SignedSweeps.card_wordOrbit_le line 84
  13. def OAI.SignedSweeps.wordPositionEquiv line 95
  14. lemma OAI.SignedSweeps.wordPositionEquiv_apply line 102
  15. def OAI.SignedSweeps.wordPositionMatrix line 105
  16. def OAI.SignedSweeps.wordTensorMatrix line 109
  17. lemma OAI.SignedSweeps.wordTensorMatrix_mul line 112
  18. lemma OAI.SignedSweeps.wordTensorMatrix_one line 119
  19. lemma OAI.SignedSweeps.wordTensorMatrix_star line 129
  20. def OAI.SignedSweeps.wordCommutant line 134
  21. lemma OAI.SignedSweeps.mem_wordCommutant_iff line 141
  22. lemma OAI.SignedSweeps.wordCommutant_histogram_constant line 159
  23. def OAI.SignedSweeps.wordOrbitMatrix line 168
  24. lemma OAI.SignedSweeps.range_wordOrbitMatrix line 174
  25. theorem OAI.SignedSweeps.span_wordTensorMatrix line 193
  26. theorem OAI.SignedSweeps.wordCommutant_finrank_le line 212