OAI/Analysis/BiholderTransport/Coordinates/SplitAction.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakMTWTransport.shifted_injectivityDomain_near_one line 121
2. lemma OAI.WeakMTWTransport.exists_minimizing_two_regular_legs line 135
3. def OAI.WeakMTWTransport.splitNormalAction line 150
4. lemma OAI.WeakMTWTransport.normalCost_le_splitNormalAction line 159
5. lemma OAI.WeakMTWTransport.splitNormalAction_contact line 166
6. lemma OAI.WeakMTWTransport.splitNormalAction_contDiffAt line 181