OAI/Analysis/RieszRectifiability/Kernel/ScalarRieszTestBounds.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Bounds for symmetric scalar Riesz tests

Derivative bounds control the symmetric test kernel near the origin, and Schwartz seminorms control its far-field decay. The resulting inverse-distance majorants establish integrability by splitting into a unit ball and its closed exterior.

  1. theorem OAI.RieszRectifiability.symmetricScalarRieszTestKernel_near_bound line 22
  2. theorem OAI.RieszRectifiability.schwartz_value_radial_bound line 64
  3. theorem OAI.RieszRectifiability.symmetricScalarRieszTestKernel_far_bound line 79
  4. theorem OAI.RieszRectifiability.symmetricScalarRieszTestKernel_integrable line 107