OAI/Analysis/BiholderTransport/Regularity/RayAnchor.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakMTWTransport.minimizing_ray_tail_cost line 20
2. def OAI.WeakMTWTransport.transformRayDifference line 30
3. lemma OAI.WeakMTWTransport.transformRayDifference_lipschitzOn line 33
4. lemma OAI.WeakMTWTransport.transformRayDifference_hasDerivAt line 45
5. lemma OAI.WeakMTWTransport.modified_ray_difference_lower line 58
6. lemma OAI.WeakMTWTransport.modified_active_norm_identity line 70
7. lemma OAI.WeakMTWTransport.modified_right_active_deficit line 84