OAI/MeasureTheory/Falconer/Shells/LocalizedScalarShell.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Scalar shell comparison from the actual localized square integral

No global bound on the oscillatory expression is used. The positive cutoff dominates the target shell, so integrability under its density gives target shell integrability and the same exact dimensional normalization.

  1. theorem OAI.Falconer.source_shell_weighted_integrable line 15
  2. theorem OAI.Falconer.localized_dyadic_shell_domination line 44
  3. theorem OAI.Falconer.localized_scalar_shell_from_angular_energy line 86