OAI/MeasureTheory/Falconer/Angular/SphereNonstationary.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A nonstationary estimate for the actual sphere measure

The amplitude is supported in one gnomonic cap. Ordinary one-coordinate regularity and a phase lower bound give arbitrary repeated-integration decay, with a constant independent of the cap amplitude and frequency. The density and the remaining-coordinate integration are included.

  1. def OAI.Falconer.chartAmplitude line 20
  2. theorem OAI.Falconer.sphere_chart_nonstationary line 23