OAI/MeasureTheory/Falconer/Angular/LongitudinalCrossTerm.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The longitudinal error for the original four endpoint transforms

The radial estimate is applied before absolute values or spatial summation. The endpoint symbols may be merely measurable in the spatial labels.

  1. theorem OAI.Falconer.longitudinal_endpoint_cross_term line 17