OAI/Analysis/FreeWords/OperatorRows.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KKFreeWords.RowSqBound line 17
  2. def OAI.KKFreeWords.ColSqBound line 20
  3. def OAI.KKFreeWords.MatrixSqBound line 23
  4. theorem OAI.KKFreeWords.RowSqBound.norm_le line 26
  5. theorem OAI.KKFreeWords.RowSqBound.star_col line 37
  6. theorem OAI.KKFreeWords.RowSqBound.reindex line 66
  7. theorem OAI.KKFreeWords.RowSqBound.prod line 72
  8. theorem OAI.KKFreeWords.row_matrix_col line 86
  9. def OAI.KKFreeWords.tupleOp line 100
  10. theorem OAI.KKFreeWords.tupleOp_row line 103
  11. theorem OAI.KKFreeWords.ColSqBound.reindex line 119
  12. theorem OAI.KKFreeWords.ColSqBound.prod line 126
  13. theorem OAI.KKFreeWords.tupleOp_col line 139
  14. theorem OAI.KKFreeWords.row_matrix_col_norm line 155
  15. theorem OAI.KKFreeWords.matrixSqBound_iff line 166
  16. theorem OAI.KKFreeWords.MatrixSqBound.add line 178
  17. theorem OAI.KKFreeWords.norm_sum_sq_le_card line 194
  18. theorem OAI.KKFreeWords.projection_sum_norm_sq line 200
  19. theorem OAI.KKFreeWords.sum_incidence line 223
  20. theorem OAI.KKFreeWords.projection_incidence_bound line 232
  21. theorem OAI.KKFreeWords.scalar_matrix_bound line 285
  22. theorem OAI.KKFreeWords.MatrixSqBound.compress line 315
  23. theorem OAI.KKFreeWords.MatrixSqBound.smul line 331