OAI/Analysis/BiholderTransport/Geodesics/ShortGradient.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakMTWTransport.exists_local_spray_cost_gradient line 86
2. lemma OAI.WeakMTWTransport.sprayFlow_reverse line 102
3. lemma OAI.WeakMTWTransport.exists_local_spray_cost_start_gradient line 106
4. lemma OAI.WeakMTWTransport.contMDiff_fiber_embedding line 146
5. lemma OAI.WeakMTWTransport.contMDiff_spray_fiber line 163
6. lemma OAI.WeakMTWTransport.spray_action_line_stationary line 169