OAI/NumberTheory/PowerFree/WeightedHypersurfaces.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.QuarticPowerFree.firstSlab_apply line 10
  2. theorem OAI.QuarticPowerFree.secondSlab_apply line 11
  3. theorem OAI.QuarticPowerFree.thirdSlab_apply line 12
  4. theorem OAI.QuarticPowerFree.mem_firstSlabs line 14
  5. theorem OAI.QuarticPowerFree.mem_secondSlabs line 31
  6. theorem OAI.QuarticPowerFree.mem_thirdSlabs line 52
  7. theorem OAI.QuarticPowerFree.card_indexedSlabs line 76
  8. theorem OAI.QuarticPowerFree.weightedNormal_card_slabs line 89
  9. theorem OAI.QuarticPowerFree.weightedPairs_shift_volume_error line 126
  10. theorem OAI.QuarticPowerFree.weightedPairs_shift_sum_error line 147
  11. def OAI.QuarticPowerFree.normalErrorConst line 172
  12. theorem OAI.QuarticPowerFree.weightedNormal_volume_error line 177
  13. def OAI.QuarticPowerFree.weightedLift line 219
  14. theorem OAI.QuarticPowerFree.weightedLift_monomial line 224
  15. theorem OAI.QuarticPowerFree.weightedLift_coeff line 239
  16. theorem OAI.QuarticPowerFree.weightedLift_eval_one line 253
  17. theorem OAI.QuarticPowerFree.weightedLift_injective line 259
  18. theorem OAI.QuarticPowerFree.weightedLift_natDegree line 264
  19. theorem OAI.QuarticPowerFree.weightedTotalDegree_mul_exact line 283
  20. theorem OAI.QuarticPowerFree.finrank_of_exact line 297
  21. theorem OAI.QuarticPowerFree.filtered_principal_finrank line 306
  22. def OAI.QuarticPowerFree.weightedSpace line 344
  23. theorem OAI.QuarticPowerFree.mem_weightedSpace line 348
  24. theorem OAI.QuarticPowerFree.weightedSpace_finite line 355
  25. theorem OAI.QuarticPowerFree.weightedSpace_finrank line 361
  26. theorem OAI.QuarticPowerFree.weighted_hypersurface_finrank line 368