OAI/Analysis/TracialCohomology/MixedWords.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Mixed words for bounded Hochschild cohomology.

  1. abbrev OAI.PopaPatching.Letter line 22
  2. def OAI.PopaPatching.letterValue line 24
  3. def OAI.PopaPatching.letterDegree line 26
  4. def OAI.PopaPatching.evaluate line 28
  5. def OAI.PopaPatching.degree line 30
  6. lemma OAI.PopaPatching.evaluate_nil line 33
  7. lemma OAI.PopaPatching.evaluate_cons line 35
  8. lemma OAI.PopaPatching.degree_nil line 37
  9. lemma OAI.PopaPatching.degree_cons line 38
  10. lemma OAI.PopaPatching.letter_norm_le line 42
  11. lemma OAI.PopaPatching.evaluate_norm_le line 49
  12. lemma OAI.PopaPatching.degree_append line 60
  13. lemma OAI.PopaPatching.evaluate_append line 63
  14. lemma OAI.PopaPatching.evaluate_zero_of_degree_ne_one line 68
  15. lemma OAI.PopaPatching.evaluate_tendsto line 87
  16. def OAI.PopaPatching.Good line 100
  17. lemma OAI.PopaPatching.good_zero line 105
  18. lemma OAI.PopaPatching.good_closed line 111
  19. lemma OAI.PopaPatching.maximal_good line 124
  20. def OAI.PopaCenter.Good line 143
  21. lemma OAI.PopaCenter.good_zero line 149
  22. lemma OAI.PopaCenter.good_closed line 158
  23. lemma OAI.PopaCenter.maximal_good line 173