OAI/Geometry/WeakHessian/LocalBounds/BoundedMulLp.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessian.memLp_mul_bounded line 45
2. def OAI.WeakHessian.boundedMulLp line 56
3. lemma OAI.WeakHessian.boundedMulLp_ae line 88
4. lemma OAI.WeakHessian.realAbs_lipschitz line 103
5. def OAI.WeakHessian.slopeMixMap line 109
6. lemma OAI.WeakHessian.continuous_slopeMixMap line 117
7. lemma OAI.WeakHessian.slopeMixMap_mem_raw line 129
8. lemma OAI.WeakHessian.relaxedGradient_mix line 187