OAI/Geometry/CylinderCovering/Rational/ScheduleExpansions.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SlopeRational.weightedCost_vanishing_padding_expansion line 12
2. theorem OAI.SlopeRational.weightedCost_quadratic_padding_expansion line 24
3. theorem OAI.SlopeRational.quadratic_coefficient_limit_of_littleO line 34
4. theorem OAI.SlopeRational.weightedCost_vanishing_padding_coefficient line 46
5. theorem OAI.SlopeRational.weightedCost_quadratic_padding_coefficient line 53