OAI/Analysis/RieszRectifiability/Foundations/SourceNormalizedRegionData.lean

Normalized height data on bounded projection regions

Uniform square-integral and fractional-energy bounds on balls restrict to the bounded projection regions inside them. Choosing bounds at each region's outer radius produces constants indexed by the region size, independent of the sequence index. Positivity of the integrands and monotonicity of restricted product measures preserve both estimates.