OAI/Analysis/RieszRectifiability/Kernel/FarRieszTransform.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The scalar far Riesz transform

Subtracting the kernel at the localization center gives an integrable far-field kernel under global upper growth. Quantitative decay bounds yield measurability and local L² control of its scalar integral on the inner ball.

  1. def OAI.RieszRectifiability.scalarFarRieszTransform line 21
  2. theorem OAI.RieszRectifiability.scalar_far_kernel_bound line 25
  3. theorem OAI.RieszRectifiability.scalarFarRieszTransform_measurable line 58
  4. theorem OAI.RieszRectifiability.scalarFarRieszTransform_integrable_and_bound line 70
  5. theorem OAI.RieszRectifiability.scalarFarRieszTransform_memLp_inner_ball line 100