OAI/Analysis/FreeWords/EntryWords.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KKRelativeMatrix.entryWords line 13
  2. theorem OAI.KKRelativeMatrix.entryWords_length line 18
  3. theorem OAI.KKRelativeMatrix.entryWords_letters line 33
  4. theorem OAI.KKRelativeMatrix.sum_map_flatMap line 50
  5. def OAI.KKRelativeMatrix.scalarWord line 58
  6. theorem OAI.KKRelativeMatrix.scalarWord_cons line 61
  7. def OAI.KKRelativeMatrix.matrixWord line 64
  8. theorem OAI.KKRelativeMatrix.entryWords_sum line 68
  9. theorem OAI.KKRelativeMatrix.norm_list_sum_le line 82