OAI/MeasureTheory/FalconerCompletion/Fourier/PolynomialKernel.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Fourier kernels and oscillatory estimates.

  1. def OAI.CriticalFourierSupport.CurrentFalconer.polynomialKernel line 17
  2. theorem OAI.CriticalFourierSupport.CurrentFalconer.polynomialKernel_pos line 19
  3. theorem OAI.CriticalFourierSupport.CurrentFalconer.polynomialKernel_le_one line 23
  4. theorem OAI.CriticalFourierSupport.CurrentFalconer.continuous_polynomialKernel line 27
  5. theorem OAI.CriticalFourierSupport.CurrentFalconer.polynomialKernel_nearby line 34
  6. theorem OAI.CriticalFourierSupport.CurrentFalconer.polynomialKernel_integrable line 52
  7. theorem OAI.CriticalFourierSupport.CurrentFalconer.polynomialKernel_integral_le line 60
  8. theorem OAI.CriticalFourierSupport.CurrentFalconer.schwartz_le_polynomialKernel line 131
  9. theorem OAI.CriticalFourierSupport.CurrentFalconer.polynomialKernel_integrable_finite line 146
  10. theorem OAI.CriticalFourierSupport.CurrentFalconer.polynomialKernel_scale_comparison line 157
  11. theorem OAI.CriticalFourierSupport.CurrentFalconer.polynomialKernel_succ_radius line 170
  12. theorem OAI.CriticalFourierSupport.CurrentFalconer.polynomialKernel_annular_tail line 180
  13. theorem OAI.CriticalFourierSupport.CurrentFalconer.polynomialKernel_integrable_prod line 211
  14. theorem OAI.CriticalFourierSupport.CurrentFalconer.bounded_mul_polynomialKernel_integrable_prod line 223