OAI/NumberTheory/Ostmann/ZeroDensity/RootFreeSmoothWeight.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Smooth variation when roots are retained at the cell endpoints

  1. theorem OAI.Ostmann.polynomial_monotoneOn_no_roots line 10
  2. theorem OAI.Ostmann.ClippedPolynomialFactor.variation_no_roots line 40
  3. theorem OAI.Ostmann.smoothPolynomialWeight_variation_no_roots line 62