OAI/Geometry/CylinderCovering/Rational/Asymptotic.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SlopeRational.eventually_lt_of_quadratic_expansion line 11
2. theorem OAI.SlopeRational.fourth_order_implies_quadratic_littleO line 25
3. theorem OAI.SlopeRational.rpow_littleO_rpow_zero line 31
4. theorem OAI.SlopeRational.vanishing_padding_conditions line 47
5. theorem OAI.SlopeRational.quadratic_padding_conditions line 64
6. theorem OAI.SlopeRational.quadratic_padding_cost_lt line 74
7. theorem OAI.SlopeRational.vanishing_padding_cost_lt line 83
8. theorem OAI.SlopeRational.exists_positive_regularization_gap line 94