OAI/Geometry/HypersurfaceGerms/Differentials.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

Chart differentials and isolation of the prepared equations.

  1. abbrev OAI.AmbientMultiplicity.ChartDifferential.V line 13
  2. abbrev OAI.AmbientMultiplicity.ChartDifferential.proj line 14
  3. def OAI.AmbientMultiplicity.ChartDifferential.H line 16
  4. def OAI.AmbientMultiplicity.ChartDifferential.HX line 17
  5. def OAI.AmbientMultiplicity.ChartDifferential.HT line 18
  6. lemma OAI.AmbientMultiplicity.ChartDifferential.H_deriv line 20
  7. def OAI.AmbientMultiplicity.ChartDifferential.perturbation line 31
  8. def OAI.AmbientMultiplicity.ChartDifferential.perturbationD line 33
  9. lemma OAI.AmbientMultiplicity.ChartDifferential.perturbation_deriv line 38
  10. lemma OAI.AmbientMultiplicity.ChartDifferential.linear_three line 48
  11. lemma OAI.AmbientMultiplicity.ChartDifferential.multiplier_coordinates line 58
  12. def OAI.AmbientMultiplicity.ChartDifferential.base0 line 83
  13. def OAI.AmbientMultiplicity.ChartDifferential.base1 line 84
  14. def OAI.AmbientMultiplicity.ChartDifferential.restricted0 line 85
  15. def OAI.AmbientMultiplicity.ChartDifferential.restricted1 line 86
  16. def OAI.AmbientMultiplicity.ChartDifferential.partDeriv line 88
  17. lemma OAI.AmbientMultiplicity.ChartDifferential.base0_deriv line 90
  18. lemma OAI.AmbientMultiplicity.ChartDifferential.base1_deriv line 99
  19. lemma OAI.AmbientMultiplicity.ChartDifferential.root_base0_deriv line 109
  20. lemma OAI.AmbientMultiplicity.ChartDifferential.root_base1_deriv line 123
  21. theorem OAI.AmbientMultiplicity.ChartDifferential.critical_chart0 line 139
  22. theorem OAI.AmbientMultiplicity.ChartDifferential.critical_chart1 line 174
  23. def OAI.AmbientMultiplicity.Preparation.scaledCoeff0 line 216
  24. def OAI.AmbientMultiplicity.Preparation.scaledCoeff1 line 218
  25. lemma OAI.AmbientMultiplicity.Preparation.scaledCoeff0_analytic line 221
  26. lemma OAI.AmbientMultiplicity.Preparation.scaledCoeff1_analytic line 225
  27. lemma OAI.AmbientMultiplicity.Preparation.scaledCoeff0_zero line 230
  28. lemma OAI.AmbientMultiplicity.Preparation.scaledCoeff1_zero line 236
  29. def OAI.AmbientMultiplicity.Preparation.rescale3 line 243
  30. lemma OAI.AmbientMultiplicity.Preparation.preparedRoot0_eq line 246
  31. lemma OAI.AmbientMultiplicity.Preparation.preparedRoot1_eq line 257
  32. lemma OAI.AmbientMultiplicity.Preparation.preparedRoot0_deriv line 268
  33. lemma OAI.AmbientMultiplicity.Preparation.preparedRoot1_deriv line 276
  34. lemma OAI.AmbientMultiplicity.Preparation.preparedRoot0_graph line 284
  35. lemma OAI.AmbientMultiplicity.Preparation.preparedRoot1_graph line 298
  36. lemma OAI.AmbientMultiplicity.Preparation.root_partial_eventually_ne line 312
  37. def OAI.AmbientMultiplicity.Preparation.lift0 line 319
  38. def OAI.AmbientMultiplicity.Preparation.lift1 line 320
  39. lemma OAI.AmbientMultiplicity.Preparation.lift0_continuousAt line 322
  40. lemma OAI.AmbientMultiplicity.Preparation.lift1_continuousAt line 328
  41. lemma OAI.AmbientMultiplicity.Preparation.lift0_zero line 336
  42. lemma OAI.AmbientMultiplicity.Preparation.lift1_zero line 337
  43. theorem OAI.AmbientMultiplicity.Preparation.f5_critical_vertical_zero line 341
  44. theorem OAI.AmbientMultiplicity.Preparation.f4_critical_vertical_zero line 375