OAI/MeasureTheory/Falconer/Fourier/SmoothMask.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Smooth angular masks from buffered good sets

A finite subcollection of the normalized cap partition gives a cutoff supported inside a prescribed set. It equals one wherever a closed ball of twice the cap radius lies in that set. No regularity of the set is needed for this finite construction.

  1. def OAI.Falconer.cutoffCapCenters line 19
  2. def OAI.Falconer.capCutoffAmbient line 23
  3. theorem OAI.Falconer.capCutoffAmbient_contDiff line 27
  4. theorem OAI.Falconer.capCutoffAmbient_properties line 32