OAI/Geometry/HypersurfaceGerms/RootBounds.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Compact quartic estimates and confinement of prepared roots.

  1. def OAI.AmbientMultiplicity.InnerQuartic.rescaledQuartic line 14
  2. lemma OAI.AmbientMultiplicity.InnerQuartic.rescaledQuartic_zero line 18
  3. lemma OAI.AmbientMultiplicity.InnerQuartic.continuous_rescaledQuartic line 27
  4. lemma OAI.AmbientMultiplicity.InnerQuartic.eventually_quartic_norm_le line 34
  5. lemma OAI.AmbientMultiplicity.InnerQuartic.sqrt_quartic_bound line 62
  6. lemma OAI.AmbientMultiplicity.RootConfinement.quartic_root_bound line 79
  7. lemma OAI.AmbientMultiplicity.RootConfinement.eventually_all_roots_small line 106