OAI/Analysis/RieszRectifiability/Foundations/SourceNormalizedEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform energy of normalized source heights

Dyadic second-moment bounds and vanishing oscillation control the fractional pair energy of normalized affine heights on each fixed ball. Eventual estimates extend to a nonnegative bound for the whole sequence, with integrability retained.

  1. theorem OAI.RieszRectifiability.source_normalized_energy_on_ball line 24