OAI/Analysis/RieszRectifiability/Kernel/CenteredShellMoments.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Second-moment and mass bounds control moments after subtracting a constant. Applying this estimate to dyadic annuli yields centered shell bounds at the prescribed geometric scale.

  1. theorem OAI.RieszRectifiability.centered_moment_from_scale line 18
  2. theorem OAI.RieszRectifiability.centered_shell_second_moment line 32
  3. theorem OAI.RieszRectifiability.cutoffMean_sq_le_amplitude line 70
  4. theorem OAI.RieszRectifiability.cutoffMean_abs_le_uniform line 81