OAI/MeasureTheory/Falconer/Slicing/OscillatoryGaussian.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Removing Gaussian damping while retaining the ambient-dimensional phase.

  1. theorem OAI.Falconer.gaussianFourierKernel_continuous_damping line 12
  2. theorem OAI.Falconer.gaussianFourierKernel_integral_limit line 32
  3. theorem OAI.Falconer.gaussian_integral_damping_limit line 53
  4. theorem OAI.Falconer.gaussian_oscillatory_pairing line 82
  5. theorem OAI.Falconer.gaussian_fresnel_coefficient line 96
  6. theorem OAI.Falconer.gaussian_stationary_identity line 119