OAI/Analysis/RieszRectifiability/Foundations/SmoothAnnularNormalPotential.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Normal potentials from smooth annular bounds

For a measure supported in a halfspace, pairing the smooth annular Riesz transform with the normal identifies the weighted positive normal potential. Uniform bounds on these transforms control truncated potential integrals and yield integrability on the limiting ball, with bound ‖e‖ * B.

  1. theorem OAI.RieszRectifiability.smooth_annular_normal_pairing line 25
  2. theorem OAI.RieszRectifiability.positiveNormalPotential_truncated_bound_of_smooth_annuli line 51
  3. theorem OAI.RieszRectifiability.positiveNormalPotential_integrable_of_smooth_annuli line 86