OAI/Analysis/BoundedHochschild/CentralQuantization.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Central centering and projection displacement.

  1. def OAI.HochschildCentralQuantization.CentrallyCentered line 24
  2. lemma OAI.HochschildCentralQuantization.central_star line 27
  3. lemma OAI.HochschildCentralQuantization.trace_weighted_orbit_closure line 34
  4. lemma OAI.HochschildCentralQuantization.zero_mem_orbit_closure line 48
  5. lemma OAI.HochschildCentralQuantization.norm_le_of_conjugations line 62
  6. lemma OAI.HochschildCentralQuantization.norm_le_of_projection_commutators line 80
  7. lemma OAI.HochschildCentralQuantization.exists_central_projection_displacement line 102