OAI/Analysis/BiholderTransport/Geodesics/RayAdvance.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakMTWTransport.lipschitz_spray_projection line 19
2. lemma OAI.WeakMTWTransport.cTransform_ray_lipschitz line 25
3. lemma OAI.WeakMTWTransport.active_norm_deficit_deriv line 33
4. lemma OAI.WeakMTWTransport.cost_norm_surplus_deriv line 45