OAI/Geometry/RCD/Metric/EuclideanMollifierSequence.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Compact smooth mollifiers with an explicit shrinking radius

  1. def OAI.RegularPointCoordinates.euclideanMollifierRadius line 13
  2. theorem OAI.RegularPointCoordinates.euclideanMollifierRadius_pos line 15
  3. theorem OAI.RegularPointCoordinates.euclideanMollifierRadius_tendsto line 19
  4. def OAI.RegularPointCoordinates.euclideanMollifierBump line 23
  5. def OAI.RegularPointCoordinates.euclideanMollifier line 27
  6. theorem OAI.RegularPointCoordinates.euclideanMollifier_smooth line 30
  7. theorem OAI.RegularPointCoordinates.euclideanMollifier_compact line 33
  8. theorem OAI.RegularPointCoordinates.euclideanMollifier_support line 36
  9. theorem OAI.RegularPointCoordinates.euclideanMollifier_convolution_tendsto line 41
  10. theorem OAI.RegularPointCoordinates.weak_harmonic_mollification line 51