OAI/MeasureTheory/Falconer/Angular/CapSymbolBounds.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The derivative budget of an actual localized endpoint pair

The cap cutoff has scale delta, while each endpoint symbol has scale D. When D dominates the inverse radius, the full amplitude satisfies the budget required by the proved nonstationary sphere estimate. The compact chart interval is deduced from cap support.

  1. theorem OAI.Falconer.capPairAmplitude_supported_derivatives line 20