OAI/Analysis/BoundedHochschild/FiniteMoments.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Small unitary moments, reindexing and simultaneous moment sequences.

  1. def OAI.HochschildPatching.asPartialUnitary line 37
  2. lemma OAI.HochschildPatching.asPartialUnitary_coe line 41
  3. lemma OAI.HochschildPatching.asPartialUnitary_power line 42
  4. theorem OAI.HochschildPatching.exists_unitary_small_moments line 57
  5. def OAI.HochschildPatching.mapAtom line 128
  6. lemma OAI.HochschildPatching.wordCoeff_map line 130
  7. lemma OAI.HochschildPatching.mixedEval_map line 132
  8. lemma OAI.HochschildPatching.admissibleTail_map line 145
  9. def OAI.HochschildPatching.coeffNumber line 155
  10. def OAI.HochschildPatching.wordCoeffNumber line 156
  11. lemma OAI.HochschildPatching.wordCoeff_smul line 158
  12. lemma OAI.HochschildPatching.mixedEval_smul line 161
  13. theorem OAI.HochschildPatching.exists_small_moment_sequence line 196