OAI/Analysis/TracialCohomology/CenterTrace.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Center trace for bounded Hochschild cohomology.

  1. def OAI.PopaCenter.Central line 23
  2. lemma OAI.PopaCenter.central_star line 25
  3. lemma OAI.PopaCenter.central_sub line 31
  4. lemma OAI.PopaCenter.central_mul line 34
  5. def OAI.PopaCenter.average line 41
  6. lemma OAI.PopaCenter.average_norm line 43
  7. lemma OAI.PopaCenter.average_central line 46
  8. lemma OAI.PopaCenter.average_orbit line 49
  9. lemma OAI.PopaCenter.central_pair_hull line 58
  10. lemma OAI.PopaCenter.central_pair_closure line 78
  11. lemma OAI.PopaCenter.average_pair line 97
  12. lemma OAI.PopaCenter.central_unique line 104
  13. lemma OAI.PopaCenter.average_eq line 110
  14. lemma OAI.PopaCenter.average_id line 116
  15. lemma OAI.PopaCenter.average_add line 118
  16. lemma OAI.PopaCenter.average_smul line 127
  17. def OAI.PopaCenter.expectation line 134
  18. lemma OAI.PopaCenter.expectation_apply line 139
  19. lemma OAI.PopaCenter.average_bimodule line 142
  20. lemma OAI.PopaCenter.average_trace line 148
  21. lemma OAI.PopaCenter.trace_average line 155
  22. lemma OAI.PopaCenter.average_nonneg line 171
  23. lemma OAI.PopaCenter.average_gns_norm line 192
  24. lemma OAI.PopaCenter.average_mono line 205
  25. lemma OAI.PopaCenter.support_central line 213
  26. lemma OAI.PopaCenter.projection_zero_of_trace_zero line 227
  27. lemma OAI.PopaCenter.projection_le_support_average line 232
  28. lemma OAI.PopaCenter.exists_central_support line 244
  29. lemma OAI.PopaCenter.maximal_separates line 289
  30. lemma OAI.PopaCenter.central_rank_trace line 312
  31. theorem OAI.PopaCenter.exists_full_initial_of_central_cuts line 319
  32. theorem OAI.PopaCenter.exists_full_initial_of_average_le line 348
  33. theorem OAI.PopaCenter.equivalent_of_average_eq line 367