OAI/MeasureTheory/Falconer/Angular/CapLocalization.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Nonstationarity on a geometric cap after point replacement

The frame depends only on the cap center and center displacement. Support and the phase lower bound are proved from the geometric cap and the original point-replacement error. Only amplitude regularity remains as local analytic data.

  1. theorem OAI.Falconer.failed_cap_sphere_nonstationary line 19