OAI/Analysis/FreeEntropy/MatrixBlockEnergy.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FiniteEntropySeparation.small_rows_bound line 10
  2. theorem OAI.FiniteEntropySeparation.clustered_energy_lower line 21
  3. theorem OAI.FiniteEntropySeparation.hermitian_row_energy line 71
  4. theorem OAI.FiniteEntropySeparation.hermitian_row_fourth line 78
  5. theorem OAI.FiniteEntropySeparation.hermitian_entry_symmetric line 90
  6. theorem OAI.FiniteEntropySeparation.commutator_diagonal_entry line 94