OAI/Analysis/TracialCohomology/PartialRepresentations.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Partial representations for bounded Hochschild cohomology.

  1. structure OAI.PopaPatching.Rep line 19
  2. instance OAI.PopaPatching.Rep.(instance at line 27) line 27
  3. def OAI.PopaPatching.Rep.support line 28
  4. lemma OAI.PopaPatching.Rep.support_mul line 31
  5. lemma OAI.PopaPatching.Rep.mul_support line 34
  6. lemma OAI.PopaPatching.Rep.support_projection line 37
  7. lemma OAI.PopaPatching.Rep.star_mul_self line 42
  8. lemma OAI.PopaPatching.Rep.mul_star_self line 45
  9. lemma OAI.PopaPatching.Rep.norm_le line 48
  10. def OAI.PopaPatching.Rep.zero line 53
  11. def OAI.PopaPatching.Rep.add line 58
  12. lemma OAI.PopaPatching.Rep.add_apply line 79
  13. lemma OAI.PopaPatching.Rep.add_support line 81