OAI/MeasureTheory/Falconer/Shells/ShellNonstationary.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Integrating angular nonstationarity over the actual radial shell

The frequency lower bound follows from the support of the fixed cutoff. No frequency assumption is added to the endpoint symbols.

  1. theorem OAI.Falconer.shell_ae_radius_lower line 16
  2. theorem OAI.Falconer.shell_nonstationary_integral_bound line 25