OAI/Analysis/TracialCohomology/PatchTraces.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Patch traces for bounded Hochschild cohomology.

  1. def OAI.PopaPatching.Rep.inCorner line 22
  2. lemma OAI.PopaPatching.Rep.inCorner_coe line 32
  3. lemma OAI.PopaPatching.Rep.inCorner_norm_le line 36
  4. lemma OAI.PopaPatching.prod_norm_le line 42
  5. lemma OAI.PopaPatching.prod_gns_sub_le line 51
  6. lemma OAI.PopaPatching.prod_gns_sub_uniform line 77
  7. lemma OAI.PopaPatching.corner_scalar_norm_le line 86
  8. lemma OAI.PopaPatching.trace_rescale line 94
  9. lemma OAI.PopaPatching.trace_product_compress line 101
  10. lemma OAI.PopaPatching.scalar_product line 136
  11. theorem OAI.PopaPatching.block_trace_error line 147
  12. lemma OAI.PopaCenter.cyclic_product_compress line 201
  13. lemma OAI.PopaCenter.central_list_prod line 236
  14. lemma OAI.PopaCenter.compress_central line 243
  15. lemma OAI.PopaCenter.central_product line 249
  16. theorem OAI.PopaCenter.block_average_error line 275