OAI/MeasureTheory/FalconerCompletion/Fourier/HalfDimensionalFourierWithCutoff.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Fourier kernels and oscillatory estimates.

  1. theorem OAI.CriticalFourierSupport.CurrentFalconer.halfDimensional_fourier_with_cutoff line 22
  2. theorem OAI.CriticalFourierSupport.CurrentFalconer.integral_div_le line 79
  3. def OAI.CriticalFourierSupport.CurrentFalconer.manuscriptFourier line 100
  4. theorem OAI.CriticalFourierSupport.CurrentFalconer.manuscriptFourier_eq_normalized line 103
  5. theorem OAI.CriticalFourierSupport.CurrentFalconer.halfDimensional_manuscriptFourier_with_cutoff line 109
  6. theorem OAI.CriticalFourierSupport.CurrentFalconer.exists_schwartz_cutoff_ball line 140
  7. theorem OAI.CriticalFourierSupport.CurrentFalconer.manuscriptFourier_norm_translate line 169
  8. theorem OAI.CriticalFourierSupport.CurrentFalconer.translate_measure_ball line 174
  9. theorem OAI.CriticalFourierSupport.CurrentFalconer.halfDimensional_fourier line 182
  10. def OAI.GraphLiteralSupport.CurrentFalconer.Exceptional.projectionCollision line 230
  11. lemma OAI.GraphLiteralSupport.CurrentFalconer.Exceptional.projectionCollision_measurable line 233
  12. lemma OAI.GraphLiteralSupport.CurrentFalconer.Exceptional.projectionCollision_le_one line 240
  13. lemma OAI.GraphLiteralSupport.CurrentFalconer.Exceptional.projectionCollision_integrable line 244
  14. lemma OAI.GraphLiteralSupport.CurrentFalconer.Exceptional.charFun_projection line 251
  15. lemma OAI.GraphLiteralSupport.CurrentFalconer.Exceptional.projectionCollision_map line 259
  16. lemma OAI.GraphLiteralSupport.CurrentFalconer.Exceptional.projection_collision_frequency_bound line 271