OAI/Geometry/WeakHessian/LocalBounds/QuadraticPotentials.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakHessian.compactCTransform line 16
2. lemma OAI.WeakHessian.compactCTransform_attained line 19
3. lemma OAI.WeakHessian.compactCTransform_le line 29
4. lemma OAI.WeakHessian.half_cost_difference_bound line 35
5. lemma OAI.WeakHessian.compactCTransform_difference_bound line 50
6. lemma OAI.WeakHessian.compactCTransform_lipschitzOn_ball line 68
7. lemma OAI.WeakHessian.compactCTransform_contact line 82