OAI/Analysis/RieszRectifiability/Kernel/MeanZeroFarTestEstimate.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Mean-zero decay of the far test integral

Subtracting the kernel value at the origin exposes a first-moment bound. The mean-zero hypothesis replaces the remaining far-region integral by its complement, whose distance from the origin gives the same extra decay power.

  1. theorem OAI.RieszRectifiability.mean_zero_far_test_integral_bound line 20