OAI/Geometry/WeakHessian/Transport/PlanIncrement.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakHessian.planMoment line 19
2. def OAI.WeakHessian.planGradientEnergy line 20
3. def OAI.WeakHessian.planKineticCost line 22
4. lemma OAI.WeakHessian.planGradientEnergy_nonneg line 25
5. lemma OAI.WeakHessian.planKineticCost_nonneg line 28
6. lemma OAI.WeakHessian.IsTestPlan.plan_increment_bound line 31
7. lemma OAI.WeakHessian.lipschitzWith_clampTime line 94
8. lemma OAI.WeakHessian.monotone_clampTime_coe line 100
9. lemma OAI.WeakHessian.IsTestPlan.uniform_plan_increment line 103