OAI/Geometry/WeakHessian/LocalBounds/LocalizedSlopeGraphMap.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessian.localSlope_congr_nhds line 47
2. lemma OAI.WeakHessian.localSlope_const line 54
3. lemma OAI.WeakHessian.localSlope_zero_of_notMem_tsupport line 57
4. lemma OAI.WeakHessian.localSlope_toReal_product_le line 63
5. lemma OAI.WeakHessian.localSlope_toReal_bound line 79
6. lemma OAI.WeakHessian.slopeGraph_localized line 86
7. def OAI.WeakHessian.localizedSlopeGraphMap line 146
8. lemma OAI.WeakHessian.continuous_localizedSlopeGraphMap line 151
9. lemma OAI.WeakHessian.relaxedGraph_localized line 159