OAI/MeasureTheory/Falconer/Graphs/GraphLiftJacobian.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.PlanarFalconer.GraphLiftSpace line 11
2. def OAI.PlanarFalconer.graphLiftMap line 13
3. def OAI.PlanarFalconer.graphLiftMatrix line 16
4. def OAI.PlanarFalconer.graphLiftDerivative line 21
5. theorem OAI.PlanarFalconer.graphLiftMap_hasFDerivAt line 24
6. theorem OAI.PlanarFalconer.graphLiftDerivative_det line 48
7. theorem OAI.PlanarFalconer.graphLiftMap_injective line 58
8. theorem OAI.PlanarFalconer.graphLiftMap_lintegral line 74