OAI/Analysis/RieszRectifiability/Kernel/ShellHeightL1.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

First-moment bounds on dyadic shells

Cauchy–Schwarz bounds an absolute first moment by the mass and second moment of a finite measure. Applying this estimate to dyadic annuli combines upper growth with shellwise second-moment decay to control the corresponding height integral.

  1. theorem OAI.RieszRectifiability.integral_abs_sq_le_mass_second_moment line 21
  2. theorem OAI.RieszRectifiability.integral_abs_le_of_mass_second_moment line 29
  3. theorem OAI.RieszRectifiability.shell_height_l1_bound line 42