OAI/Analysis/RieszRectifiability/Kernel/BlowupNormalMoments.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Normal-height moments under blowup

Positive normal height is homogeneous of degree one. Combining this with the measure's blowup normalization gives the moment scaling identity and bounds the rescaled height integral by the positive normal potential on the original ball.

  1. theorem OAI.RieszRectifiability.positiveNormalHeight_continuous line 22
  2. theorem OAI.RieszRectifiability.positiveNormalHeight_smul line 27
  3. theorem OAI.RieszRectifiability.positiveNormalHeight_integrableOn_ball line 31
  4. theorem OAI.RieszRectifiability.blowup_positiveNormalHeight_integral line 37
  5. theorem OAI.RieszRectifiability.positiveNormalHeight_eq_potential_weight line 51
  6. theorem OAI.RieszRectifiability.blowup_positiveNormalHeight_le_potential_integral line 60