OAI/Geometry/WeakHessian/Geodesics/SquareControl.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessian.IsGeodesic.squareControl line 50
2. lemma OAI.WeakHessian.IsGeodesic.ae_metricSpeed_le line 58
3. lemma OAI.WeakHessian.BoundedTracks.integrable_length_sq line 64
4. lemma OAI.WeakHessian.IsLocalWeakUpperGradient.geodesic_young line 79
5. lemma OAI.WeakHessian.IsLocalWeakUpperGradient.geodesic_young_time line 132
6. lemma OAI.WeakHessian.IsTestPlan.continuous_gradient_energy line 161
7. lemma OAI.WeakHessian.IsTestPlan.tendsto_average_gradient_energy line 173