OAI/Analysis/RieszRectifiability/Kernel/ScalarRieszSpatialDomination.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Spatial domination of scalar capped transforms

A uniform local bound and the mean-zero tail estimate combine into a measurable, nonnegative majorant for compactly supported Schwartz tests. Global upper growth makes this majorant integrable against the ambient measure, uniformly in the positive truncation scales bounded by the support radius.

  1. theorem OAI.RieszRectifiability.exists_integrable_scalarCappedTransform_dominator line 22