OAI/Analysis/RieszRectifiability/Limits/CompactSmoothAnnularKernel.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Compactly supported smooth annular kernel tests

Annular cutoffs remove the Riesz singularity and give compact support. Agreement with a capped kernel proves continuity, so pairing with a fixed normal produces a compactly supported continuous scalar test for weak limits.

  1. def OAI.RieszRectifiability.smoothAnnularKernel line 22
  2. theorem OAI.RieszRectifiability.annularSmoothBallCutoff_translate line 26
  3. theorem OAI.RieszRectifiability.smoothAnnularWeight_translate line 32
  4. theorem OAI.RieszRectifiability.smoothAnnularKernel_translate line 37
  5. theorem OAI.RieszRectifiability.smoothAnnularKernel_zero_near line 44
  6. theorem OAI.RieszRectifiability.smoothAnnularKernel_zero_far line 51
  7. theorem OAI.RieszRectifiability.smoothAnnularKernel_eq_capped line 58
  8. theorem OAI.RieszRectifiability.smoothAnnularKernel_continuous line 72
  9. theorem OAI.RieszRectifiability.smoothAnnularKernel_hasCompactSupport line 88
  10. def OAI.RieszRectifiability.scalarSmoothAnnularTest line 94