OAI/Analysis/RieszRectifiability/Limits/CompactRieszInteriorLimit.lean

Interior Riesz pairings under compact-test convergence

Restricting to a ball with zero boundary mass converts compact-test convergence into weak convergence of finite measures. Common upper growth bounds then give convergence of the interior Riesz pairing against bounded Lipschitz tests. For compactly supported mean-zero limit tests, a bump with nonzero integral also controls the mean correction, so the corrected pairings converge to the original limit pairing.