OAI/Geometry/HypersurfaceGerms/PlaneIsolation.lean

GitHub source file

82 declarations, 0 contain sorry, 0 declared as axioms

Isolation for the plane curve and its prepared pullbacks.

  1. def OAI.AmbientMultiplicity.PlaneAnalytic.q1 line 17
  2. def OAI.AmbientMultiplicity.PlaneAnalytic.q2 line 18
  3. def OAI.AmbientMultiplicity.PlaneAnalytic.q1u line 20
  4. def OAI.AmbientMultiplicity.PlaneAnalytic.q1w line 24
  5. def OAI.AmbientMultiplicity.PlaneAnalytic.q2u line 28
  6. def OAI.AmbientMultiplicity.PlaneAnalytic.q2w line 29
  7. def OAI.AmbientMultiplicity.PlaneAnalytic.d0 line 31
  8. def OAI.AmbientMultiplicity.PlaneAnalytic.d0u line 32
  9. def OAI.AmbientMultiplicity.PlaneAnalytic.d0w line 33
  10. def OAI.AmbientMultiplicity.PlaneAnalytic.psi0 line 35
  11. def OAI.AmbientMultiplicity.PlaneAnalytic.psi0u line 36
  12. def OAI.AmbientMultiplicity.PlaneAnalytic.psi0w line 37
  13. def OAI.AmbientMultiplicity.PlaneAnalytic.psi line 39
  14. def OAI.AmbientMultiplicity.PlaneAnalytic.psix line 40
  15. def OAI.AmbientMultiplicity.PlaneAnalytic.psiw line 41
  16. def OAI.AmbientMultiplicity.PlaneAnalytic.d1 line 43
  17. def OAI.AmbientMultiplicity.PlaneAnalytic.d1x line 44
  18. def OAI.AmbientMultiplicity.PlaneAnalytic.d1w line 47
  19. abbrev OAI.AmbientMultiplicity.PlaneAnalytic.B line 51
  20. def OAI.AmbientMultiplicity.PlaneAnalytic.P0 line 52
  21. def OAI.AmbientMultiplicity.PlaneAnalytic.Q0 line 53
  22. def OAI.AmbientMultiplicity.PlaneAnalytic.P1 line 54
  23. def OAI.AmbientMultiplicity.PlaneAnalytic.Q1 line 55
  24. def OAI.AmbientMultiplicity.PlaneAnalytic.res0 line 56
  25. def OAI.AmbientMultiplicity.PlaneAnalytic.res1 line 57
  26. def OAI.AmbientMultiplicity.PlaneAnalytic.mod11 line 59
  27. lemma OAI.AmbientMultiplicity.PlaneAnalytic.eleven_zero line 62
  28. lemma OAI.AmbientMultiplicity.PlaneAnalytic.P0_degree line 65
  29. lemma OAI.AmbientMultiplicity.PlaneAnalytic.Q0_degree line 69
  30. lemma OAI.AmbientMultiplicity.PlaneAnalytic.P1_degree line 73
  31. lemma OAI.AmbientMultiplicity.PlaneAnalytic.Q1_degree line 77
  32. def OAI.AmbientMultiplicity.PlaneAnalytic.P0mod line 81
  33. def OAI.AmbientMultiplicity.PlaneAnalytic.Q0mod line 82
  34. def OAI.AmbientMultiplicity.PlaneAnalytic.A0mod line 83
  35. def OAI.AmbientMultiplicity.PlaneAnalytic.B0mod line 84
  36. lemma OAI.AmbientMultiplicity.PlaneAnalytic.P0_map line 85
  37. lemma OAI.AmbientMultiplicity.PlaneAnalytic.Q0_map line 89
  38. lemma OAI.AmbientMultiplicity.PlaneAnalytic.coprime0 line 93
  39. lemma OAI.AmbientMultiplicity.PlaneAnalytic.P0mod_degree line 98
  40. lemma OAI.AmbientMultiplicity.PlaneAnalytic.Q0mod_degree line 102
  41. lemma OAI.AmbientMultiplicity.PlaneAnalytic.res0_nonzero line 106
  42. def OAI.AmbientMultiplicity.PlaneAnalytic.P1mod line 113
  43. def OAI.AmbientMultiplicity.PlaneAnalytic.Q1mod line 114
  44. def OAI.AmbientMultiplicity.PlaneAnalytic.A1mod line 115
  45. def OAI.AmbientMultiplicity.PlaneAnalytic.B1mod line 116
  46. lemma OAI.AmbientMultiplicity.PlaneAnalytic.P1_map line 117
  47. lemma OAI.AmbientMultiplicity.PlaneAnalytic.Q1_map line 121
  48. lemma OAI.AmbientMultiplicity.PlaneAnalytic.coprime1 line 125
  49. lemma OAI.AmbientMultiplicity.PlaneAnalytic.P1mod_degree line 130
  50. lemma OAI.AmbientMultiplicity.PlaneAnalytic.Q1mod_degree line 134
  51. lemma OAI.AmbientMultiplicity.PlaneAnalytic.res1_nonzero line 138
  52. lemma OAI.AmbientMultiplicity.PlaneAnalytic.polynomial_isolate_zero line 145
  53. lemma OAI.AmbientMultiplicity.PlaneAnalytic.intPolynomial_isolate_zero line 155
  54. lemma OAI.AmbientMultiplicity.PlaneAnalytic.eval_resultant_zero line 162
  55. lemma OAI.AmbientMultiplicity.PlaneAnalytic.P0_eval line 174
  56. lemma OAI.AmbientMultiplicity.PlaneAnalytic.Q0_eval line 178
  57. lemma OAI.AmbientMultiplicity.PlaneAnalytic.critical_res0 line 182
  58. lemma OAI.AmbientMultiplicity.PlaneAnalytic.P1_eval line 188
  59. lemma OAI.AmbientMultiplicity.PlaneAnalytic.Q1_eval line 192
  60. lemma OAI.AmbientMultiplicity.PlaneAnalytic.critical_res1 line 196
  61. def OAI.AmbientMultiplicity.PlaneAnalytic.sliceUnit1 line 202
  62. lemma OAI.AmbientMultiplicity.PlaneAnalytic.d1x_slice line 204
  63. theorem OAI.AmbientMultiplicity.PlaneAnalytic.d0_gradient_isolated line 210
  64. theorem OAI.AmbientMultiplicity.PlaneAnalytic.d1_gradient_isolated line 223
  65. lemma OAI.AmbientMultiplicity.PlaneAnalytic.q1_deriv line 239
  66. lemma OAI.AmbientMultiplicity.PlaneAnalytic.q2_deriv line 249
  67. lemma OAI.AmbientMultiplicity.PlaneAnalytic.d0_deriv line 258
  68. lemma OAI.AmbientMultiplicity.PlaneAnalytic.psi0_deriv line 266
  69. lemma OAI.AmbientMultiplicity.PlaneAnalytic.psi_deriv line 275
  70. lemma OAI.AmbientMultiplicity.PlaneAnalytic.d1_deriv line 283
  71. abbrev OAI.AmbientMultiplicity.Preparation.planeFst line 297
  72. abbrev OAI.AmbientMultiplicity.Preparation.planeSnd line 298
  73. def OAI.AmbientMultiplicity.Preparation.planeEmbed line 300
  74. def OAI.AmbientMultiplicity.Preparation.planeSlice line 303
  75. lemma OAI.AmbientMultiplicity.Preparation.planeEmbed_slice line 306
  76. lemma OAI.AmbientMultiplicity.Preparation.f5_plane line 311
  77. lemma OAI.AmbientMultiplicity.Preparation.f4_plane line 325
  78. lemma OAI.AmbientMultiplicity.Preparation.two_partials_zero line 337
  79. lemma OAI.AmbientMultiplicity.Preparation.f5_plane_critical_isolated line 343
  80. lemma OAI.AmbientMultiplicity.Preparation.f4_plane_critical_isolated line 362
  81. theorem OAI.AmbientMultiplicity.Preparation.f5_critical_isolated line 382
  82. theorem OAI.AmbientMultiplicity.Preparation.f4_critical_isolated line 394