OAI/MeasureTheory/Falconer/Slicing/GaussianAmplification.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Undoing Gaussian damping on a bounded original probability

  1. def OAI.Falconer.gaussianAmplifiedMeasure line 12
  2. theorem OAI.Falconer.gaussianAmplifiedMeasure_le line 15
  3. theorem OAI.Falconer.gaussianAmplifiedMeasure_finite line 27
  4. theorem OAI.Falconer.gaussianDampedMeasure_amplified line 35
  5. theorem OAI.Falconer.gaussianAmplifiedMeasure_ball_bound line 47