OAI/NumberTheory/PowerFree/DeformedRoots.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.QuarticPowerFree.mv_eval_sub_dvd line 15
  2. theorem OAI.QuarticPowerFree.mv_eval_sub_linear_dvd line 28
  3. theorem OAI.QuarticPowerFree.mv_eval_substitute line 54
  4. def OAI.QuarticPowerFree.implicitApprox line 62
  5. theorem OAI.QuarticPowerFree.eval_implicitApprox_succ line 67
  6. theorem OAI.QuarticPowerFree.implicitApprox_zero line 76
  7. theorem OAI.QuarticPowerFree.implicit_map_contraction line 93
  8. theorem OAI.QuarticPowerFree.implicitApprox_error_dvd line 109
  9. def OAI.QuarticPowerFree.implicitJacobian line 130
  10. def OAI.QuarticPowerFree.normalizedImplicitMap line 134
  11. theorem OAI.QuarticPowerFree.normalizedImplicitMap_zero line 139
  12. theorem OAI.QuarticPowerFree.normalizedImplicitMap_linear line 146
  13. theorem OAI.QuarticPowerFree.normalizedImplicitMap_fixed line 161
  14. theorem OAI.QuarticPowerFree.smooth_patch_polynomial_approx line 168
  15. theorem OAI.QuarticPowerFree.implicitApprox_eval_dvd line 184
  16. theorem OAI.QuarticPowerFree.implicitApprox_step_dvd line 193
  17. theorem OAI.QuarticPowerFree.implicitApprox_later_dvd line 212
  18. theorem OAI.QuarticPowerFree.exists_implicit_powerSeries_fixed line 226
  19. theorem OAI.QuarticPowerFree.normalizedImplicitMap_root line 275
  20. theorem OAI.QuarticPowerFree.exists_implicit_powerSeries_root line 291
  21. def OAI.QuarticPowerFree.shiftedParameterPolynomial line 302
  22. theorem OAI.QuarticPowerFree.eval_shiftedParameterPolynomial line 306
  23. theorem OAI.QuarticPowerFree.pderiv_shiftedParameterPolynomial line 317
  24. theorem OAI.QuarticPowerFree.exists_deformed_powerSeries_root line 331