OAI/MeasureTheory/Falconer/Shells/FiniteShellIntegrability.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Square integrability of the finite stationary sum

The radial coefficients need only be bounded almost everywhere on the source shell. No global bound at zero or negative frequency is required.

  1. theorem OAI.Falconer.finite_weighted_sum_sq_integrable line 14
  2. theorem OAI.Falconer.finite_spatial_shell_sq_integrable line 35