OAI/Geometry/WeakHessian/Measure/OptimalTimeLawSupported.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessian.optimalTimeLaw_supported_ball line 52
2. theorem OAI.WeakHessian.CurvatureDimension.exists_entropy_improving_sharp_midpoint line 63
3. lemma OAI.WeakHessian.endpointCost_eq_ofReal_integral line 112
4. lemma OAI.WeakHessian.optimal_cost_integral_eq line 126
5. theorem OAI.WeakHessian.CurvatureDimension.exists_entropy_bounded_midpoint line 141