OAI/MeasureTheory/Falconer/Fourier/SmoothKernel.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarFalconer.sourceBump line 11
  2. def OAI.PlanarFalconer.sourceMollifier line 17
  3. theorem OAI.PlanarFalconer.sourceMollifier_nonneg line 20
  4. theorem OAI.PlanarFalconer.sourceMollifier_smooth line 23
  5. theorem OAI.PlanarFalconer.sourceMollifier_compact line 26
  6. theorem OAI.PlanarFalconer.sourceMollifier_support line 29
  7. theorem OAI.PlanarFalconer.sourceMollifier_integral line 33
  8. instance OAI.PlanarFalconer.sourceMollifier_probability line 36
  9. theorem OAI.PlanarFalconer.sourceMollifier_ae_ball line 45
  10. theorem OAI.PlanarFalconer.sourceMollifier_test_tendsto line 54
  11. theorem OAI.PlanarFalconer.sourceMollifier_energy_le line 72