OAI/Analysis/BiholderTransport/Coordinates/CoordinateMatrices.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WeakMTWTransport.coordinateCenterMatrix line 19
2. lemma OAI.WeakMTWTransport.coordinatePoleMatrix_chart line 25
3. lemma OAI.WeakMTWTransport.coordinateCenterMatrix_chart line 36
4. lemma OAI.WeakMTWTransport.graphCoordinate_normalSubdifferential line 50
5. lemma OAI.WeakMTWTransport.WeakMTW.graphCoordinate_prefix_regular line 59