OAI/Analysis/BoundedHochschild/CenterPowers.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Center-valued weak cancellation for unitary powers.

  1. def OAI.HochschildMatrixSystems.MatrixSystem.diagonalInflate line 24
  2. lemma OAI.HochschildMatrixSystems.MatrixSystem.coefficient_compress line 42
  3. lemma OAI.HochschildMatrixSystems.MatrixSystem.coefficient_diagonal_norm line 50
  4. lemma OAI.HochschildMatrixSystems.MatrixSystem.center_coefficient_diagonal line 67
  5. lemma OAI.HochschildMatrixSystems.MatrixSystem.center_diagonal_norm line 77
  6. lemma OAI.HochschildMatrixSystems.MatrixSystem.center_root_parseval line 87
  7. lemma OAI.HochschildMatrixSystems.MatrixSystem.center_root_energy_bound line 96
  8. lemma OAI.HochschildMatrixSystems.MatrixSystem.exists_root_center_energy line 114
  9. theorem OAI.HochschildMatrixSystems.exists_unitary_center_weak_powers line 145