OAI/MeasureTheory/Falconer/Estimates/SmoothCompositionScale.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PlanarFalconer.compositionDerivativeCost line 15
2. theorem OAI.PlanarFalconer.compositionDerivativeCost_nonneg line 18
3. theorem OAI.PlanarFalconer.compositionDerivativeCost_continuous line 23
4. theorem OAI.PlanarFalconer.composition_derivative_scale line 31
5. def OAI.PlanarFalconer.weightedCompositionCost line 47
6. theorem OAI.PlanarFalconer.weightedCompositionCost_nonneg line 50
7. theorem OAI.PlanarFalconer.weightedCompositionCost_continuous line 57
8. theorem OAI.PlanarFalconer.weighted_composition_derivative_scale line 66
9. theorem OAI.PlanarFalconer.compact_weighted_composition_scale line 92