OAI/Geometry/WeakHessian/Calculus/LipschitzDerivQuadraticRemainder.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessian.lipschitzOn_deriv_quadratic_remainder line 46
2. lemma OAI.WeakHessian.hasFDerivWithinAt_integral_lipschitzOn line 68
3. lemma OAI.WeakHessian.hasFDerivAt_integral_quadratic line 119