OAI/Analysis/BoundedHochschild/RelativeCenter.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Relative central quantization and residual center bounds.

  1. def OAI.HochschildCentralQuantization.residualCenter line 25
  2. theorem OAI.HochschildCentralQuantization.exists_relative_center_order_corner line 30
  3. lemma OAI.HochschildCentralQuantization.residualCenter_of_center_mass_unit line 89
  4. lemma OAI.HochschildCentralQuantization.residualCenter_norm_of_unit line 129
  5. lemma OAI.HochschildCentralQuantization.exists_center_mass_unit line 143
  6. lemma OAI.HochschildCentralQuantization.residualCenter_norm_of_mass_floor line 166
  7. lemma OAI.HochschildCentralQuantization.centerExpectation_cyclic line 176
  8. lemma OAI.HochschildCentralQuantization.centerExpectation_compression line 188
  9. lemma OAI.HochschildCentralQuantization.residualCenter_norm_complement line 192
  10. lemma OAI.HochschildCentralQuantization.exists_positive_central_mass_band line 204