OAI/Analysis/RieszRectifiability/Nets/ExteriorCellMeans.lean

Means of exterior hard-truncated fields

For bounded data supported outside a ball, the far-kernel estimate controls the directional oscillation of the hard-truncated transform near the ball's center. Averaging this estimate over a measurable set of finite positive mass gives the same bound for the difference between its cell mean and the central value.