OAI/Geometry/WeakHessian/LocalBounds/SquareControl.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakHessian.IsSquareControl line 35
2. lemma OAI.WeakHessian.IsSquareControl.intervalIntegrable line 41
3. lemma OAI.WeakHessian.evalReal_of_mem line 46
4. lemma OAI.WeakHessian.IsSquareControl.dist_le_primitive line 53
5. lemma OAI.WeakHessian.metricSpeed_le_of_deriv_control line 74
6. lemma OAI.WeakHessian.IsSquareControl.metricSpeed_le line 90
7. lemma OAI.WeakHessian.IsSquareControl.isAC2 line 109