OAI/Geometry/WeakHessian/Transport/CouplingCostBound.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessian.IsCoupling.interpolation_endpoints line 58
2. lemma OAI.WeakHessian.IsGeodesic.hasControlBound line 68
3. lemma OAI.WeakHessian.IsGeodesic.kineticAction_le line 81
4. lemma OAI.WeakHessian.geodesic_plan_action_le_cost line 86
5. lemma OAI.WeakHessian.hasSecondMoment_of_compact line 95
6. def OAI.WeakHessian.CouplingCostBound line 109
7. lemma OAI.WeakHessian.CurvatureDimension.dynamicActionBound line 113
8. lemma OAI.WeakHessian.CurvatureDimension.testPlan_of_cost line 125