OAI/MeasureTheory/Falconer/Graphs/GraphAmplitudeSupport.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PlanarFalconer.graphAmplitudeCompact line 10
2. theorem OAI.PlanarFalconer.graphAmplitudeCompact_isCompact line 13
3. theorem OAI.PlanarFalconer.graphAmplitudePullback_norm_transport line 17
4. theorem OAI.PlanarFalconer.graphAmplitudePullback_tsupport line 27
5. theorem OAI.PlanarFalconer.graphAmplitudePullback_hasCompactSupport line 44
6. theorem OAI.PlanarFalconer.GraphDerivativeBound.global_smooth line 51
7. theorem OAI.PlanarFalconer.GraphDerivativeBound.global_bound line 67