OAI/Geometry/WeakHessian/LocalBounds/LocalizedScaling.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakHessian.localActionLimit line 16
2. lemma OAI.WeakHessian.localizedActionBound_nonneg line 19
3. lemma OAI.WeakHessian.localizedActionBound_scaled line 26
4. lemma OAI.WeakHessian.localizedActionBound_scaling_limit line 38
5. lemma OAI.WeakHessian.localized_small_scaled_eventually line 50
6. lemma OAI.WeakHessian.curvatureTailBound_scaled line 65
7. lemma OAI.WeakHessian.curvatureTailBound_scaling_limit line 87
8. lemma OAI.WeakHessian.localActionLimit_slope_limit line 103
9. lemma OAI.WeakHessian.eventually_local_scaling_admissible line 115