OAI/MeasureTheory/Falconer/Angular/AngularNearSum.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PlanarFalconer.angularPairTerm line 10
2. def OAI.PlanarFalconer.angularRestrictedSum line 13
3. theorem OAI.PlanarFalconer.angularRestrictedSum_complement line 18
4. theorem OAI.PlanarFalconer.angularRestrictedSum_schur line 29
5. theorem OAI.PlanarFalconer.angularNearSum_bound line 55