OAI/MeasureTheory/FalconerCompletion/Fourier/FourierSubLeft.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Fourier kernels and oscillatory estimates.

  1. theorem OAI.CriticalFourierSupport.CurrentFalconer.fourier_sub_left line 22
  2. theorem OAI.CriticalFourierSupport.CurrentFalconer.sourceFourier_reproduce line 41
  3. theorem OAI.CriticalFourierSupport.CurrentFalconer.weighted_integral_sq_le line 61
  4. theorem OAI.CriticalFourierSupport.CurrentFalconer.sourceFourier_sq_le_smooth line 93
  5. theorem OAI.CriticalFourierSupport.CurrentFalconer.gaussianBallSeries_summable line 119
  6. def OAI.CriticalFourierSupport.CurrentFalconer.gaussianBallConstant line 143
  7. theorem OAI.CriticalFourierSupport.CurrentFalconer.gaussianBallConstant_nonneg line 146
  8. theorem OAI.CriticalFourierSupport.CurrentFalconer.gaussian_integral_le_ball_series line 154
  9. theorem OAI.CriticalFourierSupport.CurrentFalconer.gaussian_integral_le_ball_bound line 215
  10. theorem OAI.CriticalFourierSupport.CurrentFalconer.probability_ball_bound_large_radii line 242
  11. theorem OAI.CriticalFourierSupport.CurrentFalconer.gaussian_distance_integrable line 269
  12. theorem OAI.CriticalFourierSupport.CurrentFalconer.gaussian_fourier_integral_le line 276
  13. theorem OAI.CriticalFourierSupport.CurrentFalconer.fourier_ball_integral_le line 318