OAI/Analysis/FreeEntropy/MatrixChart.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FiniteEntropySeparation.hermitianMatrix_add line 9
  2. theorem OAI.FiniteEntropySeparation.hermitianMatrix_smul line 14
  3. def OAI.FiniteEntropySeparation.hermitianChart line 19
  4. theorem OAI.FiniteEntropySeparation.hermitianMatrix_isHermitian line 23
  5. theorem OAI.FiniteEntropySeparation.hermitianMatrix_normSq line 33
  6. theorem OAI.FiniteEntropySeparation.hermitianMatrix_frobenius line 45
  7. theorem OAI.FiniteEntropySeparation.hermitianChart_normSq line 53
  8. theorem OAI.FiniteEntropySeparation.hermitianMatrix_continuous line 58
  9. theorem OAI.FiniteEntropySeparation.matrixMoment_continuous line 61