OAI/MeasureTheory/Falconer/Estimates/SpatialAnnulusKernel.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Smooth annular inverse-distance kernels in the ambient Euclidean space.

  1. def OAI.Falconer.spatialInnerBump line 16
  2. def OAI.Falconer.spatialOuterBump line 19
  3. def OAI.Falconer.spatialAnnulusKernel line 22
  4. theorem OAI.Falconer.spatialAnnulusKernel_smooth line 26
  5. theorem OAI.Falconer.spatialAnnulusKernel_compact line 42
  6. theorem OAI.Falconer.spatialAnnulusKernel_eq line 47
  7. def OAI.Falconer.spatialAnnulusSchwartz line 56