OAI/Geometry/WeakHessian/Sobolev/QuadraticGradient.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakHessian.QuadraticLipschitzBound line 18
2. lemma OAI.WeakHessian.QuadraticLipschitzBound.lipschitzOn_ball line 21
3. lemma OAI.WeakHessian.QuadraticLipschitzBound.continuous line 36
4. lemma OAI.WeakHessian.QuadraticLipschitzBound.deriv_comp_bound line 43
5. lemma OAI.WeakHessian.QuadraticLipschitzBound.comp_ac line 70
6. lemma OAI.WeakHessian.QuadraticLipschitzBound.endpoint_bound line 78
7. lemma OAI.WeakHessian.QuadraticLipschitzBound.upperGradient line 95
8. lemma OAI.WeakHessian.QuadraticLipschitzBound.localSobolev line 115
9. lemma OAI.WeakHessian.QuadraticLipschitzBound.gradient_le line 125