OAI/Geometry/HypersurfaceGerms/Orders.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Exact orders four and five of the prepared holomorphic germs.

  1. lemma OAI.AmbientMultiplicity.Preparation.coordinate_vanishing line 15
  2. lemma OAI.AmbientMultiplicity.Preparation.q1_vanishing line 18
  3. lemma OAI.AmbientMultiplicity.Preparation.psi_vanishing line 25
  4. def OAI.AmbientMultiplicity.Preparation.chartUnit0 line 33
  5. def OAI.AmbientMultiplicity.Preparation.chartUnit1 line 34
  6. lemma OAI.AmbientMultiplicity.Preparation.chartUnit0_analytic line 35
  7. lemma OAI.AmbientMultiplicity.Preparation.chartUnit1_analytic line 39
  8. lemma OAI.AmbientMultiplicity.Preparation.chartUnit0_one line 43
  9. lemma OAI.AmbientMultiplicity.Preparation.chartUnit1_one line 44
  10. lemma OAI.AmbientMultiplicity.Preparation.chartUnit0_remainder line 45
  11. lemma OAI.AmbientMultiplicity.Preparation.chartUnit1_remainder line 47
  12. def OAI.AmbientMultiplicity.Preparation.quadratic line 50
  13. lemma OAI.AmbientMultiplicity.Preparation.quadratic_vanishing line 51
  14. def OAI.AmbientMultiplicity.Preparation.error0 line 54
  15. def OAI.AmbientMultiplicity.Preparation.error1 line 55
  16. lemma OAI.AmbientMultiplicity.Preparation.error0_vanishing line 57
  17. lemma OAI.AmbientMultiplicity.Preparation.error1_vanishing line 67
  18. lemma OAI.AmbientMultiplicity.Preparation.eliminated0_vanishing line 76
  19. lemma OAI.AmbientMultiplicity.Preparation.eliminated1_vanishing line 80
  20. lemma OAI.AmbientMultiplicity.Preparation.perturbation_vanishing line 85
  21. def OAI.AmbientMultiplicity.Preparation.initial5 line 94
  22. def OAI.AmbientMultiplicity.Preparation.initial4 line 95
  23. lemma OAI.AmbientMultiplicity.Preparation.initial5_vanishing line 96
  24. lemma OAI.AmbientMultiplicity.Preparation.initial4_vanishing line 99
  25. lemma OAI.AmbientMultiplicity.Preparation.f5_remainder line 102
  26. lemma OAI.AmbientMultiplicity.Preparation.f4_remainder line 112
  27. lemma OAI.AmbientMultiplicity.Preparation.initial5_nonzero line 125
  28. lemma OAI.AmbientMultiplicity.Preparation.initial4_nonzero line 133
  29. theorem OAI.AmbientMultiplicity.Preparation.order_five line 142
  30. theorem OAI.AmbientMultiplicity.Preparation.order_four line 148