OAI/Analysis/BoundedHochschild/CenterEnergy.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Matrix displacement and central energy estimates.

  1. lemma OAI.HochschildCentralQuantization.exists_colored_matrix_displacement line 25
  2. theorem OAI.HochschildMatrixSystems.MatrixSystem.exists_central_energy_decreasing_extension line 74
  3. theorem OAI.HochschildCentralQuantization.exists_small_matrix_expectations line 152