OAI/NumberTheory/PiExponent/Approximation/WeightedSliceDegree.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponent.WeightedSliceDegree.SupportBound line 11
  2. theorem OAI.PiExponent.WeightedSliceDegree.SupportBound.mono line 14
  3. theorem OAI.PiExponent.WeightedSliceDegree.supportBound_zero line 18
  4. theorem OAI.PiExponent.WeightedSliceDegree.supportBound_C line 23
  5. theorem OAI.PiExponent.WeightedSliceDegree.supportBound_X line 30
  6. theorem OAI.PiExponent.WeightedSliceDegree.SupportBound.add line 38
  7. theorem OAI.PiExponent.WeightedSliceDegree.SupportBound.mul line 46
  8. theorem OAI.PiExponent.WeightedSliceDegree.SupportBound.pow line 53
  9. theorem OAI.PiExponent.WeightedSliceDegree.supportBound_prod line 60
  10. theorem OAI.PiExponent.WeightedSliceDegree.supportBound_sum line 71
  11. theorem OAI.PiExponent.WeightedSliceDegree.supportBound_aeval_monomial line 82
  12. theorem OAI.PiExponent.WeightedSliceDegree.supportBound_aeval line 95
  13. def OAI.PiExponent.WeightedSliceDegree.sliceMap line 105
  14. theorem OAI.PiExponent.WeightedSliceDegree.sliceMap_X_mem line 110
  15. theorem OAI.PiExponent.WeightedSliceDegree.sliceMap_X_notMem line 115
  16. theorem OAI.PiExponent.WeightedSliceDegree.sliceMap_C line 120
  17. theorem OAI.PiExponent.WeightedSliceDegree.sliceMap_eval line 125
  18. theorem OAI.PiExponent.WeightedSliceDegree.supportBound_sliceMap line 135
  19. theorem OAI.PiExponent.WeightedSliceDegree.supportBound_sliceMap_sum line 151
  20. theorem OAI.PiExponent.WeightedSliceDegree.supportBound_renameEquiv line 160
  21. def OAI.PiExponent.WeightedSliceDegree.enumeratedSliceMap line 169
  22. theorem OAI.PiExponent.WeightedSliceDegree.supportBound_enumeratedSliceMap line 173
  23. theorem OAI.PiExponent.WeightedSliceDegree.supportBound_enumeratedSliceMap_sum line 181
  24. theorem OAI.PiExponent.WeightedSliceDegree.enumeratedSliceMap_eval line 190