OAI/Analysis/RieszRectifiability/Foundations/SmoothAnnularWeights.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Smooth annular and exterior weights

Differences of smooth ball cutoffs localize functions to annular regions. Subtracting a cutoff from a finite-measure set indicator gives an exterior weight with controlled size, square integrability, and distance from the center.

  1. def OAI.RieszRectifiability.annularSmoothBallCutoff line 21
  2. def OAI.RieszRectifiability.smoothAnnularWeight line 24
  3. def OAI.RieszRectifiability.smoothExteriorWeight line 27
  4. theorem OAI.RieszRectifiability.annularSmoothBallCutoff_basic line 31
  5. theorem OAI.RieszRectifiability.annularSmoothBallCutoff_energy line 45
  6. theorem OAI.RieszRectifiability.smoothAnnularWeight_properties line 54
  7. theorem OAI.RieszRectifiability.smoothExteriorWeight_properties line 83
  8. theorem OAI.RieszRectifiability.smoothAnnularWeights_sum line 113