OAI/Analysis/BiholderTransport/Geodesics/SprayProjection.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.WeakMTWTransport.hasMFDerivAt_spray_projection line 82
  2. lemma OAI.WeakMTWTransport.spray_velocity_eq_mfderiv line 107
  3. def OAI.WeakMTWTransport.sprayFlow line 118
  4. lemma OAI.WeakMTWTransport.sprayFlow_zero line 121
  5. lemma OAI.WeakMTWTransport.sprayFlow_curve line 124
  6. lemma OAI.WeakMTWTransport.sprayFlow_add line 128
  7. lemma OAI.WeakMTWTransport.contMDiff_sprayFlow line 133
  8. lemma OAI.WeakMTWTransport.sprayFlow_speed line 139
  9. lemma OAI.WeakMTWTransport.tangent_chart_target_iff line 155
  10. lemma OAI.WeakMTWTransport.hasMFDerivAt_of_coordinate_spray line 169
  11. lemma OAI.WeakMTWTransport.coordinate_geodesic_scale line 186
  12. lemma OAI.WeakMTWTransport.sprayFlow_eq_coordinate_curve line 205