OAI/MeasureTheory/Falconer/Fourier/StationaryFactorShell.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The normalized finite stationary expansion in the original shell

Total inverse order pays the derivative order of both endpoint factors. The remaining constants are fixed before the cell scale and radial variable.

  1. theorem OAI.Falconer.stationary_factor_shell_le line 17