OAI/Analysis/TracialCohomology/CenterExtensions.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Center extensions for bounded Hochschild cohomology.

  1. lemma OAI.PopaCenter.closedCommutant_typeII line 26
  2. lemma OAI.PopaCenter.conjugate_of_average_eq line 92
  3. def OAI.PopaCenter.System.conjugated line 138
  4. lemma OAI.PopaCenter.System.conjugated_expect line 145
  5. lemma OAI.PopaCenter.System.conjugated_commutes line 154
  6. theorem OAI.PopaCenter.exists_matrix_approximating_projection_center line 175
  7. lemma OAI.PopaCenter.center_distance_le_projection_commutators line 238
  8. theorem OAI.PopaCenter.exists_large_projection_commutator_center line 272
  9. theorem OAI.PopaCenter.exists_matrix_energy_decrease_center line 288
  10. lemma OAI.PopaCenter.average_expect line 323
  11. lemma OAI.PopaCenter.extend_energy_decrease_center line 335