OAI/MeasureTheory/Falconer/Graphs/GraphWeightDerivatives.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PlanarFalconer.graphBinPullback line 9
2. def OAI.PlanarFalconer.graphConePullback line 13
3. def OAI.PlanarFalconer.graphWeightPullback line 16
4. theorem OAI.PlanarFalconer.graph_bin_derivative_budget line 21
5. theorem OAI.PlanarFalconer.graph_cone_derivative_budget line 45
6. theorem OAI.PlanarFalconer.graphWeightPullback_distance line 52
7. theorem OAI.PlanarFalconer.graphWeightPullback_product line 62
8. theorem OAI.PlanarFalconer.graph_source_weight_derivative_budget line 73