OAI/MeasureTheory/Falconer/Slicing/GaussianLebesgue.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A Lebesgue density for the standard Gaussian used in the band estimates

  1. def OAI.Falconer.gaussianLebesgue line 13
  2. instance OAI.Falconer.gaussianLebesgue_finite line 16
  3. theorem OAI.Falconer.gaussianLebesgue_sourceFourier line 23
  4. def OAI.Falconer.gaussianVolumeNormalization line 43
  5. def OAI.Falconer.normalizedGaussianLebesgue line 45
  6. instance OAI.Falconer.normalizedGaussianLebesgue_finite line 48
  7. theorem OAI.Falconer.normalizedGaussianLebesgue_sourceFourier line 53