OAI/MeasureTheory/Falconer/Graphs/GraphDerivativeBounds.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.PlanarFalconer.GraphDerivativeBound line 10
2. theorem OAI.PlanarFalconer.GraphDerivativeBound.mul line 15
3. theorem OAI.PlanarFalconer.GraphDerivativeBound.conj line 26
4. theorem OAI.PlanarFalconer.GraphDerivativeBound.mono line 34
5. theorem OAI.PlanarFalconer.GraphDerivativeBound.congr line 42
6. theorem OAI.PlanarFalconer.graph_fixed_derivative_budget line 56
7. theorem OAI.PlanarFalconer.graph_periodic_derivative_budget line 67