OAI/Analysis/RieszRectifiability/Kernel/ExpandingSmoothCutoffs.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Expanding smooth cutoffs

Dilating a fixed bump gives compactly supported smooth cutoffs equal to one on balls of increasing radius. Composition with linear contractions bounds all derivatives by Schwartz seminorms and supplies uniform derivative bounds for the cutoff errors.

  1. def OAI.RieszRectifiability.unitSmoothCutoff line 22
  2. def OAI.RieszRectifiability.expandingSmoothCutoff line 25
  3. theorem OAI.RieszRectifiability.expandingSmoothCutoff_smooth line 28
  4. theorem OAI.RieszRectifiability.expandingSmoothCutoff_compact line 33
  5. theorem OAI.RieszRectifiability.expandingSmoothCutoff_one line 45
  6. theorem OAI.RieszRectifiability.schwartz_contraction_derivative_bound line 57
  7. theorem OAI.RieszRectifiability.expandingSmoothCutoff_error_uniform_derivatives line 69