OAI/Analysis/FreeWords/TupleMatrices.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KKFreeWords.tupleScalarMatrix line 19
  2. theorem OAI.KKFreeWords.tupleScalarMatrix_bound line 24
  3. def OAI.KKFreeWords.tupleProjectionMatrix line 42
  4. def OAI.KKFreeWords.tupleMissingWeight line 46
  5. theorem OAI.KKFreeWords.tupleProjectionMatrix_bound line 50
  6. theorem OAI.KKFreeWords.tupleMissingWeight_rows line 70
  7. theorem OAI.KKFreeWords.tupleMissingWeight_cols line 75
  8. theorem OAI.KKFreeWords.tupleMissingMatrix_bound line 83
  9. def OAI.KKFreeWords.tuplePresMatrix line 91
  10. theorem OAI.KKFreeWords.tuplePresMatrix_eq line 96
  11. theorem OAI.KKFreeWords.tuplePresMatrix_bound line 112