OAI/Analysis/FreeEntropy/MatrixOperator.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FiniteEntropySeparation.matrixOperator line 11
  2. theorem OAI.FiniteEntropySeparation.matrixOperator_mul line 13
  3. theorem OAI.FiniteEntropySeparation.matrixOperator_one line 17
  4. theorem OAI.FiniteEntropySeparation.matrixOperator_add line 20
  5. theorem OAI.FiniteEntropySeparation.matrixOperator_smul line 24
  6. theorem OAI.FiniteEntropySeparation.matrixOpNorm_nonneg line 28
  7. theorem OAI.FiniteEntropySeparation.matrixOpNorm_mul line 29
  8. theorem OAI.FiniteEntropySeparation.matrixOpNorm_one line 34
  9. theorem OAI.FiniteEntropySeparation.matrixOpNorm_add line 38
  10. theorem OAI.FiniteEntropySeparation.matrixOpNorm_smul line 43
  11. theorem OAI.FiniteEntropySeparation.matrixOpNorm_prod line 47
  12. theorem OAI.FiniteEntropySeparation.matrixOpNorm_word line 54
  13. theorem OAI.FiniteEntropySeparation.matrix_entry_bound line 64
  14. theorem OAI.FiniteEntropySeparation.matrix_trace_bound line 72
  15. theorem OAI.FiniteEntropySeparation.matrix_normalized_trace_bound line 78