OAI/NumberTheory/PowerFree/CurveThresholds.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.QuarticPowerFree.coordinateLinearForm line 11
  2. theorem OAI.QuarticPowerFree.coordinateLinearForm_weighted line 15
  3. theorem OAI.QuarticPowerFree.conjugateLinePolynomial_aeval line 30
  4. theorem OAI.QuarticPowerFree.norm_polynomial_line_degrees line 40
  5. theorem OAI.QuarticPowerFree.norm_polynomial_line_hilbert line 91
  6. theorem OAI.QuarticPowerFree.polynomial_coordinates_injOn line 126
  7. theorem OAI.QuarticPowerFree.norm_curve_alternatives line 141
  8. def OAI.QuarticPowerFree.normBoxEnvelope line 230
  9. def OAI.QuarticPowerFree.normBoxStage line 236
  10. def OAI.QuarticPowerFree.normBoxIncrement line 237
  11. theorem OAI.QuarticPowerFree.normBoxEnvelope_pos line 240
  12. theorem OAI.QuarticPowerFree.normBox_generic_certificate line 244
  13. theorem OAI.QuarticPowerFree.normBox_full_certificate line 249
  14. theorem OAI.QuarticPowerFree.normBox_curve_certificate line 253
  15. theorem OAI.QuarticPowerFree.normBox_increment_nonneg_5 line 257
  16. theorem OAI.QuarticPowerFree.normBox_prefix_5 line 260
  17. theorem OAI.QuarticPowerFree.normBox_sum_5 line 264
  18. theorem OAI.QuarticPowerFree.normBox_increment_nonneg_6 line 268
  19. theorem OAI.QuarticPowerFree.normBox_prefix_6 line 271
  20. theorem OAI.QuarticPowerFree.normBox_sum_6 line 275
  21. theorem OAI.QuarticPowerFree.normBox_increment_nonneg_7 line 279
  22. theorem OAI.QuarticPowerFree.normBox_prefix_7 line 282
  23. theorem OAI.QuarticPowerFree.normBox_sum_7 line 286
  24. theorem OAI.QuarticPowerFree.normBox_increment_nonneg_8 line 290
  25. theorem OAI.QuarticPowerFree.normBox_prefix_8 line 293
  26. theorem OAI.QuarticPowerFree.normBox_sum_8 line 297
  27. theorem OAI.QuarticPowerFree.normBox_increment_nonneg line 301
  28. theorem OAI.QuarticPowerFree.normBox_prefix line 309
  29. theorem OAI.QuarticPowerFree.normBox_sum line 318
  30. theorem OAI.QuarticPowerFree.normBox_generic_threshold line 325
  31. theorem OAI.QuarticPowerFree.normBox_full_threshold line 331
  32. theorem OAI.QuarticPowerFree.normBox_curve_threshold line 336