OAI/Geometry/HypersurfaceGerms/CriticalBounds.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Quantitative local isolation estimates for critical points.

  1. def OAI.AmbientMultiplicity.CriticalEstimates.hX line 12
  2. def OAI.AmbientMultiplicity.CriticalEstimates.hT line 13
  3. def OAI.AmbientMultiplicity.CriticalEstimates.delta line 15
  4. lemma OAI.AmbientMultiplicity.CriticalEstimates.gradient_T_bound line 17
  5. lemma OAI.AmbientMultiplicity.CriticalEstimates.gradient_X_bound line 45
  6. theorem OAI.AmbientMultiplicity.CriticalEstimates.gradient_bound line 61
  7. lemma OAI.AmbientMultiplicity.CriticalEstimates.vertical_euler_relation line 74
  8. lemma OAI.AmbientMultiplicity.CriticalEstimates.vertical_multiplier_product line 96
  9. lemma OAI.AmbientMultiplicity.CriticalEstimates.vertical_multiplier_bound line 111
  10. def OAI.AmbientMultiplicity.CriticalEstimates.quartic line 129
  11. def OAI.AmbientMultiplicity.CriticalEstimates.quarticD line 130
  12. lemma OAI.AmbientMultiplicity.CriticalEstimates.quartic_euler_expansion line 133
  13. lemma OAI.AmbientMultiplicity.CriticalEstimates.quartic_euler_bound line 142
  14. def OAI.AmbientMultiplicity.CriticalEstimates.isolationConstant line 191
  15. theorem OAI.AmbientMultiplicity.CriticalEstimates.critical_nonzero_base_vertical_zero line 196
  16. theorem OAI.AmbientMultiplicity.CriticalEstimates.critical_zero_base line 256
  17. abbrev OAI.AmbientMultiplicity.LocalIsolation.V line 297
  18. abbrev OAI.AmbientMultiplicity.LocalIsolation.proj line 298
  19. theorem OAI.AmbientMultiplicity.LocalIsolation.norm_two line 300
  20. theorem OAI.AmbientMultiplicity.LocalIsolation.coefficient_bound line 311
  21. theorem OAI.AmbientMultiplicity.LocalIsolation.derivative_bound line 323
  22. abbrev OAI.AmbientMultiplicity.CriticalEstimates.V line 340
  23. def OAI.AmbientMultiplicity.CriticalEstimates.base2 line 342
  24. def OAI.AmbientMultiplicity.CriticalEstimates.preparedRoot line 344
  25. lemma OAI.AmbientMultiplicity.CriticalEstimates.quartic_deriv line 346
  26. lemma OAI.AmbientMultiplicity.CriticalEstimates.preparedRoot_analytic line 358
  27. lemma OAI.AmbientMultiplicity.CriticalEstimates.preparedRoot_u_deriv line 372
  28. def OAI.AmbientMultiplicity.CriticalEstimates.base5 line 400
  29. def OAI.AmbientMultiplicity.CriticalEstimates.ConstrainedCritical line 404
  30. theorem OAI.AmbientMultiplicity.CriticalEstimates.critical_vertical_zero line 413