OAI/Geometry/WeakHessian/Transport/RestrictCurve.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessian.IsTestPlan.restrictCurve line 20
2. lemma OAI.WeakHessian.BoundedTracks.restrictCurve line 48
3. lemma OAI.WeakHessian.action_restrictCurve line 58
4. lemma OAI.WeakHessian.IsLocalWeakUpperGradient.ae_subinterval_le line 77
5. lemma OAI.WeakHessian.IsTestPlan.lintegral_eval_le line 95
6. lemma OAI.WeakHessian.IsTestPlan.lintegral_square_eval_lt_top line 106
7. lemma OAI.WeakHessian.ofReal_sq_le_ofReal_sq line 143
8. lemma OAI.WeakHessian.IsTestPlan.lintegral_action_lt_top line 149