OAI/Probability/SKGap/Matrix/WordIncrement.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKGap.WordLetter.close line 16
  2. def OAI.SKGap.wordHolderScale line 22
  3. lemma OAI.SKGap.wordHolderScale_ge_one line 26
  4. lemma OAI.SKGap.wordHolderScale_constants line 32
  5. lemma OAI.SKGap.WordLetter.eval_pair line 47
  6. theorem OAI.SKGap.actualWord_pair_increments line 88
  7. inductive OAI.SKGap.WordTemplateLetter line 118
  8. abbrev OAI.SKGap.WordParameter line 124
  9. def OAI.SKGap.templateInverse line 126
  10. def OAI.SKGap.templateDiagonal line 127
  11. def OAI.SKGap.WordTemplateLetter.realize line 129
  12. def OAI.SKGap.templateWord line 134
  13. def OAI.SKGap.templateScale line 137
  14. lemma OAI.SKGap.templateInverse_bounds line 140
  15. lemma OAI.SKGap.templateDiagonal_bound line 149
  16. lemma OAI.SKGap.templateWord_bounded line 157
  17. lemma OAI.SKGap.template_coord_dist line 167
  18. lemma OAI.SKGap.templateInverse_dist line 172
  19. lemma OAI.SKGap.templateLetter_close line 182
  20. lemma OAI.SKGap.templateWord_paired line 200