OAI/Geometry/WeakMTW/Geodesics/IntrinsicExp.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WeakMTWGlobalSupport.RiemannianLocal.mulState line 17
  2. theorem OAI.WeakMTWGlobalSupport.RiemannianLocal.curveState_comp_affine line 21
  3. theorem OAI.WeakMTWGlobalSupport.RiemannianLocal.intrinsic_affine_dist line 41
  4. theorem OAI.WeakMTWGlobalSupport.WeakMTW.completeGeodesic_iff_state line 74
  5. theorem OAI.WeakMTWGlobalSupport.WeakMTW.completeGeodesic_comp_mul line 90
  6. theorem OAI.WeakMTWGlobalSupport.WeakMTW.exp_eq_of_complete line 104
  7. theorem OAI.WeakMTWGlobalSupport.WeakMTW.exp_mul_eq_of_complete line 113
  8. def OAI.WeakMTWGlobalSupport.WeakMTW.geodesic line 119
  9. theorem OAI.WeakMTWGlobalSupport.WeakMTW.geodesic_complete line 122
  10. theorem OAI.WeakMTWGlobalSupport.WeakMTW.geodesic_smooth line 126
  11. theorem OAI.WeakMTWGlobalSupport.WeakMTW.geodesic_state_zero line 129
  12. theorem OAI.WeakMTWGlobalSupport.WeakMTW.geodesic_dist line 133
  13. theorem OAI.WeakMTWGlobalSupport.WeakMTW.geodesic_zero line 138
  14. theorem OAI.WeakMTWGlobalSupport.WeakMTW.exp_eq_geodesic line 141
  15. theorem OAI.WeakMTWGlobalSupport.WeakMTW.exp_mul_eq_geodesic line 144
  16. theorem OAI.WeakMTWGlobalSupport.WeakMTW.exp_zero line 147