OAI/Analysis/BiholderTransport/Coordinates/RadialIdentity.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakMTWTransport.normalCost line 113
2. lemma OAI.WeakMTWTransport.normalCost_contDiffAt line 116
3. lemma OAI.WeakMTWTransport.shifted_exp_endpoint line 124
4. lemma OAI.WeakMTWTransport.shifted_injectivityDomain_near_zero line 132
5. lemma OAI.WeakMTWTransport.normalCost_radial_fderiv_of_shift line 148
6. lemma OAI.WeakMTWTransport.normalCost_radial_fderiv_near_zero line 185
7. lemma OAI.WeakMTWTransport.normalCost_radial_hessian line 219