OAI/NumberTheory/PowerFree/WeightedSlabs.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.QuarticPowerFree.simplexPairs line 10
  2. theorem OAI.QuarticPowerFree.mem_simplexPairs line 13
  3. theorem OAI.QuarticPowerFree.card_simplexPairs line 20
  4. def OAI.QuarticPowerFree.weightedPairs line 34
  5. theorem OAI.QuarticPowerFree.mem_weightedPairs line 38
  6. theorem OAI.QuarticPowerFree.pair_divmod_injective line 48
  7. theorem OAI.QuarticPowerFree.weightedPairs_upper line 69
  8. theorem OAI.QuarticPowerFree.weightedPairs_lower line 90
  9. theorem OAI.QuarticPowerFree.weightedPairs_quadratic_bounds line 127
  10. theorem OAI.QuarticPowerFree.weightedPairs_volume_error line 174
  11. abbrev OAI.QuarticPowerFree.NatTriple line 192
  12. def OAI.QuarticPowerFree.tripleWeight line 194
  13. def OAI.QuarticPowerFree.weightedTriples line 196
  14. theorem OAI.QuarticPowerFree.mem_weightedTriples line 200
  15. def OAI.QuarticPowerFree.tripleDivides line 212
  16. instance OAI.QuarticPowerFree.(instance at line 214) line 214
  17. def OAI.QuarticPowerFree.weightedNormal line 216
  18. def OAI.QuarticPowerFree.tripleShift line 219
  19. theorem OAI.QuarticPowerFree.tripleWeight_shift line 229
  20. theorem OAI.QuarticPowerFree.weightedNormal_card_add line 235
  21. def OAI.QuarticPowerFree.firstSlab line 265
  22. def OAI.QuarticPowerFree.secondSlab line 269
  23. def OAI.QuarticPowerFree.thirdSlab line 276
  24. def OAI.QuarticPowerFree.firstSlabs line 283
  25. def OAI.QuarticPowerFree.secondSlabs line 286
  26. def OAI.QuarticPowerFree.thirdSlabs line 289