OAI/Geometry/WeakHessian/LocalBounds/RealClip.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakHessianFunctional.realClip line 28
2. lemma OAI.WeakHessianFunctional.realClip_lipschitz line 29
3. lemma OAI.WeakHessianFunctional.realClip_zero line 31
4. lemma OAI.WeakHessianFunctional.realClip_abs_le line 32
5. lemma OAI.WeakHessianFunctional.realClip_norm_le line 34
6. lemma OAI.WeakHessianFunctional.realClip_tendsto line 37
7. lemma OAI.WeakHessianFunctional.realClip_tendsto_Lp line 44