OAI/Geometry/WeakHessian/LocalBounds/AscendingSlope.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakHessian.ascendingSlope line 49
2. def OAI.WeakHessian.ascendingSlopeApprox line 51
3. lemma OAI.WeakHessian.ascendingSlope_eq_iInf line 54
4. lemma OAI.WeakHessian.ascendingSlopeApprox_le line 75
5. lemma OAI.WeakHessian.ascendingSlope_le line 87
6. lemma OAI.WeakHessian.lowerSemicontinuous_ascendingSlopeApprox line 92
7. lemma OAI.WeakHessian.measurable_ascendingSlope line 106
8. lemma OAI.WeakHessian.ascending_quotient_limsup_le line 112
9. lemma OAI.WeakHessian.deriv_comp_le_ascendingSlopeApprox line 138
10. lemma OAI.WeakHessian.deriv_comp_le_ascendingSlope line 172
11. lemma OAI.WeakHessian.ascendingSlope_isLocalWeakUpperGradient line 181
12. lemma OAI.WeakHessian.weakGradient_le_ascendingSlope line 226
13. lemma OAI.WeakHessian.ascendingSlope_le_of_quadratic_increment line 235
14. lemma OAI.WeakHessian.ascendingSlope_hopf_contact line 256
15. lemma OAI.WeakHessian.ascendingSlope_contact line 267
16. lemma OAI.WeakHessian.contact_geodesic_decrease line 279