OAI/Analysis/BoundedHochschild/CommutantQuantization.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Small matrix expectations and coefficient energy bounds.

  1. def OAI.HochschildQuantization.matrixEnergy line 40
  2. lemma OAI.HochschildQuantization.matrixEnergy_nonneg line 43
  3. lemma OAI.HochschildQuantization.matrixEnergy_drop line 46
  4. theorem OAI.HochschildQuantization.exists_small_matrix_expectations line 69
  5. lemma OAI.HochschildMatrixSystems.MatrixSystem.coefficient_product_matrix line 122
  6. lemma OAI.HochschildMatrixSystems.MatrixSystem.sum_coefficient_diagonal line 140
  7. lemma OAI.HochschildMatrixSystems.MatrixSystem.coefficient_norm_sq_sum line 148
  8. lemma OAI.HochschildMatrixSystems.MatrixSystem.trace_entry_commutant line 162