OAI/Analysis/FreeEntropy/MatrixWordDerivative.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FiniteEntropySeparation.matrixWord line 12
  2. theorem OAI.FiniteEntropySeparation.matrixWord_nil line 13
  3. theorem OAI.FiniteEntropySeparation.matrixWord_cons line 14
  4. theorem OAI.FiniteEntropySeparation.matrixWord_append line 15
  5. def OAI.FiniteEntropySeparation.matrixWordVariation line 16
  6. theorem OAI.FiniteEntropySeparation.matrixWordVariation_nil line 18
  7. theorem OAI.FiniteEntropySeparation.matrixWordVariation_cons line 19
  8. theorem OAI.FiniteEntropySeparation.hasDerivAt_matrixWord line 31
  9. theorem OAI.FiniteEntropySeparation.hasDerivAt_matrixWord_trace line 39
  10. theorem OAI.FiniteEntropySeparation.matrixWordVariation_trace line 43
  11. def OAI.FiniteEntropySeparation.cyclicMatrixWord line 51
  12. theorem OAI.FiniteEntropySeparation.cyclicMatrixWord_bound line 53