OAI/Analysis/RieszRectifiability/Kernel/SubtractedFarTestEstimate.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

First-moment control of the subtracted far test

The far-region integral splits at the ball of radius ‖x‖ / 2 about the origin. The central part uses the kernel difference estimate, while the outer part uses the first absolute moment to gain the same decay of order ‖x‖ ^ (m + 2).

  1. theorem OAI.RieszRectifiability.subtracted_far_test_integral_norm_bound line 21