OAI/Analysis/BiholderTransport/Convexity/EndpointLowerJet.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakMTWTransport.exists_smooth_normal_endpoint_log_of_nonconjugate line 22
2. lemma OAI.WeakMTWTransport.norm_reverseRay line 64
3. lemma OAI.WeakMTWTransport.exists_reverse_branch_with_forward_action line 69