OAI/MeasureTheory/Falconer/Graphs/GraphPolarJacobian.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PlanarFalconer.graphPolarMap line 10
2. def OAI.PlanarFalconer.graphPolarInverse line 13
3. def OAI.PlanarFalconer.graphPolarDomain line 16
4. def OAI.PlanarFalconer.graphPolarMatrix line 19
5. def OAI.PlanarFalconer.graphPolarDerivative line 24
6. theorem OAI.PlanarFalconer.graphPolarMap_hasFDerivAt line 27
7. theorem OAI.PlanarFalconer.graphPolarDerivative_det line 50
8. theorem OAI.PlanarFalconer.graphPolarInverse_left line 57
9. theorem OAI.PlanarFalconer.graphPolarMap_injOn line 64
10. theorem OAI.PlanarFalconer.graphPolarMap_lintegral line 68