OAI/Geometry/WeakHessian/LocalBounds/JoinCurve.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakHessian.joinCurve line 36
2. lemma OAI.WeakHessian.joinCurve_apply_left line 39
3. lemma OAI.WeakHessian.joinCurve_apply_right line 49
4. lemma OAI.WeakHessian.joinCurve_zero line 66
5. lemma OAI.WeakHessian.joinCurve_one line 74
6. abbrev OAI.WeakHessian.Joinable line 82
7. def OAI.WeakHessian.joinMap line 85
8. lemma OAI.WeakHessian.isClosed_joinable line 87
9. lemma OAI.WeakHessian.lipschitz_joinMap line 91
10. lemma OAI.WeakHessian.hasControlBound_of_squareControl line 103