OAI/Analysis/BiholderTransport/Coordinates/PoleCoordinates.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakMTWTransport.hopfLax_lipschitz line 18
2. def OAI.WeakMTWTransport.coordinateBackward line 31
3. lemma OAI.WeakMTWTransport.coordinateBackward_contMDiffAt line 35
4. lemma OAI.WeakMTWTransport.coordinateBackward_of_derivative line 50
5. lemma OAI.WeakMTWTransport.hasMFDerivAt_riemannianGradient line 79
6. def OAI.WeakMTWTransport.hopfPole line 88
7. lemma OAI.WeakMTWTransport.WeakMTW.coordinateBackward_eq_pole line 92