OAI/Analysis/BiholderTransport/Coordinates/Coordinates.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakMTWTransport.metricDual_isInvertible line 59
2. def OAI.WeakMTWTransport.coordinateChristoffel line 78
3. lemma OAI.WeakMTWTransport.coordinateChristoffel_metric line 83
4. lemma OAI.WeakMTWTransport.coordinateChristoffel_self_metric line 91
5. def OAI.WeakMTWTransport.coordinateGeodesicField line 97
6. lemma OAI.WeakMTWTransport.metric_speed_derivative line 100
7. lemma OAI.WeakMTWTransport.contDiffAt_coordinateChristoffel line 127
8. lemma OAI.WeakMTWTransport.contDiffAt_coordinateGeodesicField line 161
9. lemma OAI.WeakMTWTransport.coordinate_geodesic_speed_constant line 170