OAI/Combinatorics/SumProduct/Alignment/RationalLattice18.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RationalLattice.PolynomialArrays.integer_cover line 30
  2. lemma OAI.RationalLattice.PolynomialArrays.second_integer_cover line 66
  3. lemma OAI.RationalLattice.PolynomialArrays.lattice_level_compact_reps line 85
  4. lemma OAI.RationalLattice.PolynomialArrays.lattice_compactSpace line 102
  5. lemma OAI.RationalLattice.PolynomialArrays.lattice_quotient_t2 line 112
  6. def OAI.RationalLattice.PolynomialArrays.evaluate line 140
  7. lemma OAI.RationalLattice.PolynomialArrays.evaluate_continuous line 144
  8. lemma OAI.RationalLattice.PolynomialArrays.readout_polynomial line 147
  9. lemma OAI.RationalLattice.PolynomialArrays.evaluate_rational line 158
  10. lemma OAI.RationalLattice.PolynomialArrays.shift_coordinates line 164
  11. lemma OAI.RationalLattice.PolynomialArrays.shift_polynomial line 171
  12. lemma OAI.RationalLattice.PolynomialArrays.shift_rational line 190
  13. lemma OAI.RationalLattice.PolynomialArrays.shift_level line 197
  14. lemma OAI.RationalLattice.PolynomialArrays.evaluate_level line 208
  15. def OAI.RationalLattice.PolynomialArrays.readout line 219
  16. lemma OAI.RationalLattice.PolynomialArrays.readout_continuous line 223
  17. def OAI.RationalLattice.PolynomialArrays.shifted line 227
  18. lemma OAI.RationalLattice.PolynomialArrays.shifted_continuous line 234
  19. lemma OAI.RationalLattice.PolynomialArrays.shifted_add line 238
  20. lemma OAI.RationalLattice.PolynomialArrays.shifted_zero line 249
  21. def OAI.RationalLattice.PolynomialArrays.shiftedHomeomorph line 260
  22. lemma OAI.RationalLattice.PolynomialArrays.readout_shifted line 270