OAI/Analysis/TracialCohomology/PatchBounds.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Patch bounds for bounded Hochschild cohomology.

  1. lemma OAI.PopaPatching.rank_nonneg line 20
  2. lemma OAI.PopaPatching.rank_le_one line 22
  3. lemma OAI.PopaPatching.good_short_bound line 27
  4. lemma OAI.PopaPatching.projection_trace_real line 35
  5. lemma OAI.PopaPatching.residual_scalar line 39
  6. lemma OAI.PopaPatching.residual_scalar_bound line 48
  7. lemma OAI.PopaPatching.scalar_prod_bound line 61
  8. lemma OAI.PopaPatching.norm_list_sum_le line 73
  9. lemma OAI.PopaPatching.patch_sum_bound line 80
  10. lemma OAI.PopaCenter.preGNS_real_smul line 126
  11. lemma OAI.PopaCenter.good_short_bound line 129
  12. lemma OAI.PopaCenter.residual_coefficient line 138
  13. lemma OAI.PopaCenter.residual_coefficient_bound line 149
  14. lemma OAI.PopaCenter.product_l2_bound line 163
  15. lemma OAI.PopaCenter.norm_list_sum line 174
  16. lemma OAI.PopaCenter.patch_sum_bound line 182