OAI/Geometry/WeakMTW/Geodesics/GeodesicFlow.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakMTWGlobalSupport.WeakMTW.geodesicFlow line 21
2. theorem OAI.WeakMTWGlobalSupport.WeakMTW.geodesic_intrinsic line 24
3. theorem OAI.WeakMTWGlobalSupport.WeakMTW.geodesicFlow_zero line 28
4. theorem OAI.WeakMTWGlobalSupport.WeakMTW.geodesicFlow_norm line 30
5. theorem OAI.WeakMTWGlobalSupport.WeakMTW.geodesicFlow_continuous_time line 34
6. theorem OAI.WeakMTWGlobalSupport.WeakMTW.geodesic_shift_complete line 37
7. theorem OAI.WeakMTWGlobalSupport.WeakMTW.geodesic_shift line 49
8. theorem OAI.WeakMTWGlobalSupport.WeakMTW.geodesicFlow_add line 53
9. theorem OAI.WeakMTWGlobalSupport.WeakMTW.geodesicFlow_sub line 63