OAI/Analysis/FreeEntropy/MatrixPolynomial.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.FiniteEntropySeparation.MatrixIndex line 10
  2. def OAI.FiniteEntropySeparation.coordinateMatrix line 11
  3. theorem OAI.FiniteEntropySeparation.coordinateMatrix_polynomial line 13
  4. theorem OAI.FiniteEntropySeparation.coordinateMatrix_update line 20
  5. theorem OAI.FiniteEntropySeparation.coordinateMatrix_hasDeriv line 31
  6. def OAI.FiniteEntropySeparation.IsMatrixPolynomial line 42
  7. theorem OAI.FiniteEntropySeparation.IsMatrixPolynomial.const line 44
  8. theorem OAI.FiniteEntropySeparation.IsMatrixPolynomial.add line 45
  9. theorem OAI.FiniteEntropySeparation.IsMatrixPolynomial.mul line 47
  10. theorem OAI.FiniteEntropySeparation.IsMatrixPolynomial.smul line 51
  11. theorem OAI.FiniteEntropySeparation.IsMatrixPolynomial.trace line 53
  12. theorem OAI.FiniteEntropySeparation.IsMatrixPolynomial.word line 56
  13. theorem OAI.FiniteEntropySeparation.hasDerivAt_matrix_mul line 62