OAI/Geometry/WeakHessian/Geodesics/GeodesicPlanSupportedBall.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessian.geodesic_plan_supported_ball line 50
2. lemma OAI.WeakHessian.scaled_CD_spreading_constant line 69
3. lemma OAI.WeakHessian.CurvatureDimension.reroute_midpoint_restriction line 81
4. lemma OAI.WeakHessian.CurvatureDimension.optimalTimeLaws_nonempty line 175
5. lemma OAI.WeakHessian.CD_cap_support_cancel line 188
6. theorem OAI.WeakHessian.CurvatureDimension.exists_bounded_midpoint line 196
7. lemma OAI.WeakHessian.isClosed_probability_dominated line 275
8. lemma OAI.WeakHessian.exists_dominated_of_approximations line 289
9. theorem OAI.WeakHessian.CurvatureDimension.exists_sharply_bounded_midpoint line 332