OAI/Analysis/FreeEntropy/MatrixScoreWords.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FiniteEntropySeparation.matrixScoreWord line 10
  2. theorem OAI.FiniteEntropySeparation.matrixScoreWord_polynomial line 12
  3. theorem OAI.FiniteEntropySeparation.matrixScoreWord_derivative line 16
  4. theorem OAI.FiniteEntropySeparation.hermitianBasis_contract_trace line 40
  5. theorem OAI.FiniteEntropySeparation.matrixScoreWord_divergence line 46
  6. def OAI.FiniteEntropySeparation.matrixPolynomial line 64
  7. def OAI.FiniteEntropySeparation.matrixScorePolynomial line 66
  8. theorem OAI.FiniteEntropySeparation.matrixScorePolynomial_sum line 68
  9. theorem OAI.FiniteEntropySeparation.matrixScorePolynomial_polynomial line 72
  10. theorem OAI.FiniteEntropySeparation.matrixScorePolynomial_divergence line 77