OAI/Analysis/BiholderTransport/Geodesics/GeodesicSpray.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakMTWTransport.tangent_chart_source_iff line 71
2. lemma OAI.WeakMTWTransport.tangent_chart_transition_eventually line 86
3. lemma OAI.WeakMTWTransport.tangent_tangentCoordChange_apply line 101
4. lemma OAI.WeakMTWTransport.riemannianCoordinateMetric_isInvertible line 119
5. lemma OAI.WeakMTWTransport.riemannianMetric_transition_eventually line 125
6. def OAI.WeakMTWTransport.geodesicSpray line 150
7. lemma OAI.WeakMTWTransport.geodesicSpray_coordinates line 155
8. lemma OAI.WeakMTWTransport.contMDiff_geodesicSpray line 199