OAI/MeasureTheory/Falconer/Shells/SpatialSharedShell.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform independent-angle control removes the spatial Fourier variable

The spatial coefficient pays its squared L1 norm. All exchanges of the radial and spatial integrations follow from bounded measurable endpoint families and the finite original shell measure.

  1. def OAI.Falconer.spatialSharedAmplitude line 17
  2. theorem OAI.Falconer.spatialSharedAmplitude_measurable line 22
  3. theorem OAI.Falconer.spatial_shared_shell_le line 32
  4. theorem OAI.Falconer.spatial_fourier_shared_shell_le line 113