OAI/Combinatorics/SumProduct/Alignment/CorrectedBox06.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CorrectedBoxLeibman.translationEntry line 25
  2. def OAI.CorrectedBoxLeibman.translationMatrix line 27
  3. def OAI.CorrectedBoxLeibman.gridTranslate line 30
  4. lemma OAI.CorrectedBoxLeibman.translationEntry_low line 33
  5. lemma OAI.CorrectedBoxLeibman.translationEntry_eval line 36
  6. lemma OAI.CorrectedBoxLeibman.gridTranslate_eval line 47
  7. lemma OAI.CorrectedBoxLeibman.translationMatrix_le line 63
  8. lemma OAI.CorrectedBoxLeibman.gridTranslate_totalDegree line 69
  9. lemma OAI.CorrectedBoxLeibman.translationEntry_bound line 80
  10. lemma OAI.CorrectedBoxLeibman.translationMatrix_bound line 102
  11. lemma OAI.CorrectedBoxLeibman.gridTranslate_bound line 113
  12. lemma OAI.CorrectedBoxLeibman.grid_scale_change line 153
  13. theorem OAI.ComparableBoxLeibman.comparable_integer_box_unit line 200