OAI/Analysis/TracialCohomology/FreshBounds.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Fresh bounds for bounded Hochschild cohomology.

  1. def OAI.PopaPatching.identitySingleton line 21
  2. lemma OAI.PopaPatching.norm_trace_projection line 23
  3. lemma OAI.PopaPatching.norm_le_error line 28
  4. lemma OAI.PopaPatching.singleton_cancellation_bound line 31
  5. theorem OAI.PopaPatching.many_blocks_bound line 69
  6. lemma OAI.PopaPatching.identitySingleton_one line 130
  7. lemma OAI.PopaPatching.identitySingleton_two line 132
  8. theorem OAI.PopaPatching.all_blocks_bound line 135
  9. lemma OAI.PopaCenter.singleton_cancellation_bound line 224
  10. lemma OAI.PopaCenter.cyclic_blocks line 268
  11. theorem OAI.PopaCenter.many_blocks_bound line 314
  12. theorem OAI.PopaCenter.all_blocks_bound line 380