OAI/Geometry/WeakHessian/LocalBounds/TimeHalf.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakHessian.timeHalf line 50
2. lemma OAI.WeakHessian.cd_midpoint_support_lower line 52
3. lemma OAI.WeakHessian.map_sub_of_le line 105
4. lemma OAI.WeakHessian.replacement_map_eq line 112
5. lemma OAI.WeakHessian.replacement_probability line 117
6. lemma OAI.WeakHessian.endpointCoupling_add line 125
7. lemma OAI.WeakHessian.quadraticTransportCost_add line 130
8. lemma OAI.WeakHessian.IsOptimalCoupling.reroute_plan line 134
9. lemma OAI.WeakHessian.geodesic_plan_reroute line 165
10. lemma OAI.WeakHessian.interpolation_restricted line 171