OAI/MeasureTheory/Falconer/Angular/DyadicPerpendicular.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Perpendicular localization on actual descendant cubes

The small point-to-center error and derivative hypotheses are verified for the original cell-restricted symbols before applying the cap estimate.

  1. theorem OAI.Falconer.dyadic_perpendicular_cross_term line 17