OAI/AlgebraicGeometry/AbhyankarSathaye/CriticalPoint.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

An explicit critical point away from the zero fiber

At (h,u,v,w) = (2,0,-1/2,1/2), the value of F is -1 and every partial derivative vanishes. Differentiating the ambient polynomial identity proves the latter without expanding F.

  1. def OAI.AbhyankarSathaye.criticalPoint line 19
  2. theorem OAI.AbhyankarSathaye.criticalPoint_h line 22
  3. theorem OAI.AbhyankarSathaye.criticalPoint_u line 23
  4. theorem OAI.AbhyankarSathaye.criticalPoint_v line 24
  5. theorem OAI.AbhyankarSathaye.criticalPoint_w line 25
  6. theorem OAI.AbhyankarSathaye.eval_x line 27
  7. theorem OAI.AbhyankarSathaye.eval_y line 30
  8. theorem OAI.AbhyankarSathaye.eval_s line 33
  9. theorem OAI.AbhyankarSathaye.eval_p line 36
  10. theorem OAI.AbhyankarSathaye.eval_F line 39
  11. theorem OAI.AbhyankarSathaye.eval_shiftX line 42
  12. theorem OAI.AbhyankarSathaye.eval_shiftY line 45
  13. theorem OAI.AbhyankarSathaye.critical_of_ambient_identity line 48
  14. theorem OAI.AbhyankarSathaye.critical_derivatives line 57