OAI/Geometry/WeakHessian/LocalBounds/ExcessRelocation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessian.excess_relocation_le line 48
2. lemma OAI.WeakHessian.cappedExcess_relocation_le line 70
3. theorem OAI.WeakHessian.CurvatureDimension.exists_bounded_midpoint_preserving_caps line 78
4. theorem OAI.WeakHessian.CurvatureDimension.exists_sharp_midpoint_preserving_caps line 184
5. lemma OAI.WeakHessian.lower_dominance_of_cap_le line 230
6. theorem OAI.WeakHessian.CurvatureDimension.exists_sharp_midpoint_above_lower line 248