OAI/MeasureTheory/Falconer/Slicing/GaussianMass.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Gaussian mass at a finite Frostman scale

Only ball bounds at radii at least B⁻¹ are used. This is the spatial Gaussian estimate in the proof of the half-dimensional Fourier estimate.

  1. def OAI.Falconer.gaussianBallConstant line 17
  2. theorem OAI.Falconer.gaussianBallConstant_summable line 20
  3. theorem OAI.Falconer.gaussianBallConstant_nonneg line 36
  4. def OAI.Falconer.gaussianMassTerm line 41
  5. theorem OAI.Falconer.gaussian_pointwise_majorant line 45
  6. theorem OAI.Falconer.gaussian_mass_bound line 66