OAI/Combinatorics/SumProduct/Alignment/PairTail02.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PairTail.lowerArgs line 24
  2. def OAI.PairTail.baseInput line 28
  3. def OAI.PairTail.tailInput line 31
  4. lemma OAI.PairTail.baseInput_polynomial line 35
  5. lemma OAI.PairTail.tailCorrection_exists line 44
  6. def OAI.PairTail.tailCorrection line 72
  7. lemma OAI.PairTail.baseInput_args line 76
  8. lemma OAI.PairTail.tailInput_args line 89
  9. lemma OAI.PairTail.tailCorrection_args line 98
  10. def OAI.PairTail.correction line 132
  11. lemma OAI.PairTail.correction_base line 138
  12. lemma OAI.PairTail.correction_tail line 143
  13. lemma OAI.PairTail.coordinate_mul line 148
  14. def OAI.PairTail.reducedCoordinates line 187
  15. def OAI.RationalLattice.reduceCoordinates line 208
  16. lemma OAI.RationalLattice.reduceCoordinates_bounds line 214
  17. lemma OAI.RationalLattice.reduceCoordinates_coset line 244
  18. theorem OAI.RationalLattice.compact_reps_of_integerCoordinates line 260