OAI/Geometry/CylinderCovering/Convexity/QuadraticTaylorBound.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CylinderCovering.QuadraticTaylor.remainder_le_on_closedBall line 13
2. theorem OAI.CylinderCovering.QuadraticTaylor.exists_uniform_taylor_bound_of_bounded_hessian line 32
3. theorem OAI.CylinderCovering.QuadraticTaylor.exists_uniform_taylor_bound line 50
4. theorem OAI.CylinderCovering.QuadraticTaylor.exists_uniform_taylor_bound_near line 75
5. theorem OAI.CylinderCovering.QuadraticTaylor.exists_uniform_taylor_norm_bound_near line 84