OAI/Geometry/WeakHessian/LocalBounds/SlopeApprox.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakHessian.slopeApprox line 21
2. lemma OAI.WeakHessian.localSlope_eq_iInf_slopeApprox line 25
3. lemma OAI.WeakHessian.lowerSemicontinuous_slopeApprox line 47
4. lemma OAI.WeakHessian.measurable_localSlope line 63
5. lemma OAI.WeakHessian.slopeApprox_le_lipschitz line 69
6. lemma OAI.WeakHessian.localSlope_le_lipschitz line 82
7. lemma OAI.WeakHessian.deriv_comp_le_slopeApprox line 87
8. lemma OAI.WeakHessian.deriv_comp_le_localSlope line 132
9. lemma OAI.WeakHessian.localSlope_isLocalWeakUpperGradient line 141