OAI/Geometry/WeakHessian/Transport/RerouteFiniteSubplanShort.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessian.CurvatureDimension.reroute_finite_subplan_short line 52
2. lemma OAI.WeakHessian.CurvatureDimension.reroute_midpoint_restriction_short line 146
3. theorem OAI.WeakHessian.CurvatureDimension.exists_bounded_midpoint_preserving_caps_short line 241
4. theorem OAI.WeakHessian.CurvatureDimension.exists_sharp_midpoint_preserving_caps_short line 348
5. theorem OAI.WeakHessian.CurvatureDimension.exists_sharp_midpoint_above_lower_short line 395
6. theorem OAI.WeakHessian.CurvatureDimension.exists_entropy_improving_sharp_midpoint_short line 418
7. theorem OAI.WeakHessian.CurvatureDimension.exists_entropy_bounded_midpoint_short line 468