OAI/NumberTheory/PowerFree/PatchBounds.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.QuarticPowerFree.kernelDegreeBudget line 14
  2. def OAI.QuarticPowerFree.kernelCountBudget line 18
  3. theorem OAI.QuarticPowerFree.le_kernelDegreeBudget line 22
  4. theorem OAI.QuarticPowerFree.one_le_kernelCountBudget line 27
  5. theorem OAI.QuarticPowerFree.bounded_kernel_components line 30
  6. theorem OAI.QuarticPowerFree.affineDimension_antitone line 114
  7. theorem OAI.QuarticPowerFree.bounded_kernel_patch_cover line 123
  8. def OAI.QuarticPowerFree.stagedEvaluationSpace line 176
  9. def OAI.QuarticPowerFree.stagedKernelPolynomials line 180
  10. theorem OAI.QuarticPowerFree.stagedKernelPolynomials_degree line 185
  11. theorem OAI.QuarticPowerFree.stagedEvaluationSpace_mono line 190
  12. theorem OAI.QuarticPowerFree.mem_stagedKernelPolynomials line 194
  13. structure OAI.QuarticPowerFree.KernelGeometry line 205
  14. def OAI.QuarticPowerFree.KernelParent line 211
  15. def OAI.QuarticPowerFree.kernelChildList line 214
  16. theorem OAI.QuarticPowerFree.kernelChildList_spec line 226
  17. def OAI.QuarticPowerFree.firstCoveringChild line 246
  18. theorem OAI.QuarticPowerFree.firstCoveringChild_spec line 253
  19. def OAI.QuarticPowerFree.kernelHeightConstant line 275
  20. theorem OAI.QuarticPowerFree.kernel_height_pow_bound line 278
  21. def OAI.QuarticPowerFree.minorSizeConstant line 297
  22. def OAI.QuarticPowerFree.minorSizeExponent line 300
  23. theorem OAI.QuarticPowerFree.minorSizeConstant_nonneg line 303
  24. theorem OAI.QuarticPowerFree.bounded_minor_height line 307
  25. theorem OAI.QuarticPowerFree.uniform_patch_minor_height line 339