OAI/MeasureTheory/Falconer/Angular/FullCircleDecomposition.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PlanarFalconer.stationarySineCutoff_periodic line 10
2. theorem OAI.PlanarFalconer.stationaryCosineCutoff_periodic line 17
3. theorem OAI.PlanarFalconer.cosineOscillator_periodic line 24
4. theorem OAI.PlanarFalconer.stationaryCosineCutoff_add_pi line 28
5. theorem OAI.PlanarFalconer.cosineOscillator_add_pi line 35
6. theorem OAI.PlanarFalconer.circle_negative_piece line 41
7. theorem OAI.PlanarFalconer.circle_residual_integral line 67
8. theorem OAI.PlanarFalconer.full_circle_decomposition line 93