OAI/MeasureTheory/FalconerCompletion/Fourier/Fourier.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Fourier kernels and oscillatory estimates.

  1. def OAI.CriticalFourierSupport.PlanarFalconer.sourceFourier line 21
  2. theorem OAI.CriticalFourierSupport.PlanarFalconer.sourceFourier_integral_swap line 24
  3. theorem OAI.CriticalFourierSupport.PlanarFalconer.sourceFourier_difference line 45
  4. theorem OAI.CriticalFourierSupport.PlanarFalconer.gaussian_lebesgue_integrable line 52
  5. theorem OAI.CriticalFourierSupport.PlanarFalconer.source_gaussian_fourier line 58
  6. theorem OAI.CriticalFourierSupport.PlanarFalconer.gaussian_lebesgue_square line 75
  7. theorem OAI.CriticalFourierSupport.PlanarFalconer.source_scaled_gaussian_identity line 104
  8. theorem OAI.CriticalFourierSupport.PlanarFalconer.gaussian_sourceFourier_integrable line 123
  9. theorem OAI.CriticalFourierSupport.PlanarFalconer.source_scaled_gaussian_lintegral line 135