OAI/Analysis/BiholderTransport/Geodesics/MetricGeodesicLift.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakMTWTransport.velocity_lift_eq_of_eventuallyEq line 86
2. lemma OAI.WeakMTWTransport.metric_curve_velocity_isMIntegralCurve line 93
3. lemma OAI.WeakMTWTransport.metric_curve_eq_spray line 116
4. lemma OAI.WeakMTWTransport.geodesicWithInitialData_eq_spray line 138
5. lemma OAI.WeakMTWTransport.riemannianExp_eq_sprayFlow line 144
6. lemma OAI.WeakMTWTransport.riemannianExp_smul line 149
7. lemma OAI.WeakMTWTransport.contMDiff_riemannianExp line 156