OAI/MeasureTheory/FalconerCompletion/Fourier/FourierPolynomialSmoothing.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Fourier kernels and oscillatory estimates.

  1. theorem OAI.CriticalFourierSupport.CurrentFalconer.sourceFourier_polynomial_smoothing line 24
  2. theorem OAI.CriticalFourierSupport.CurrentFalconer.sourceFourier_norm_le_one line 77
  3. theorem OAI.CriticalFourierSupport.CurrentFalconer.sourceFourier_annular_integral line 81
  4. theorem OAI.CriticalFourierSupport.CurrentFalconer.sphere_cap_ball_bound line 197
  5. def OAI.CriticalFourierSupport.CurrentFalconer.annularScalarSet line 224
  6. theorem OAI.CriticalFourierSupport.CurrentFalconer.measurableSet_annularScalarSet line 227
  7. theorem OAI.CriticalFourierSupport.CurrentFalconer.volume_annularScalarSet_le line 232
  8. def OAI.CriticalFourierSupport.CurrentFalconer.radialWindow line 252
  9. theorem OAI.CriticalFourierSupport.CurrentFalconer.measurableSet_radialWindow line 255
  10. theorem OAI.CriticalFourierSupport.CurrentFalconer.volume_radialWindow_le line 258
  11. theorem OAI.CriticalFourierSupport.CurrentFalconer.smul_mem_ball_radialWindow line 265
  12. theorem OAI.CriticalFourierSupport.CurrentFalconer.smul_mem_ball_of_inv line 281
  13. instance OAI.CriticalFourierSupport.CurrentFalconer.finite_annularScalar line 294
  14. def OAI.CriticalFourierSupport.CurrentFalconer.annularFrequencyMeasure line 306
  15. instance OAI.CriticalFourierSupport.CurrentFalconer.finite_annularFrequencyMeasure line 310
  16. theorem OAI.CriticalFourierSupport.CurrentFalconer.annularFrequencyMeasure_mass line 315
  17. theorem OAI.CriticalFourierSupport.CurrentFalconer.annularFrequencyMeasure_support line 323
  18. theorem OAI.CriticalFourierSupport.CurrentFalconer.annularFrequencyMeasure_ball line 335