OAI/MeasureTheory/Falconer/Angular/CompactCircleResidual.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PlanarFalconer.contDiff_interval_zero_extension line 10
2. def OAI.PlanarFalconer.compactCircleResidual line 35
3. theorem OAI.PlanarFalconer.compactCircleResidual_contDiff line 38
4. theorem OAI.PlanarFalconer.compactCircleResidual_tsupport line 44
5. theorem OAI.PlanarFalconer.compactCircleResidual_sine_support line 52
6. def OAI.PlanarFalconer.circleResidualAmplitude line 62
7. theorem OAI.PlanarFalconer.circleResidualAmplitude_contDiff line 65
8. theorem OAI.PlanarFalconer.circleResidualAmplitude_support line 69