OAI/MeasureTheory/FalconerCompletion/Fourier/SpatialInnerBump.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Fourier kernels and oscillatory estimates.

  1. def OAI.GraphLiteralSupport.Attempt4PrefixShell.SpatialFourierND.spatialInnerBump line 17
  2. def OAI.GraphLiteralSupport.Attempt4PrefixShell.SpatialFourierND.spatialOuterBump line 20
  3. def OAI.GraphLiteralSupport.Attempt4PrefixShell.SpatialFourierND.spatialAnnulusKernel line 23
  4. theorem OAI.GraphLiteralSupport.Attempt4PrefixShell.SpatialFourierND.spatialAnnulusKernel_smooth line 27
  5. theorem OAI.GraphLiteralSupport.Attempt4PrefixShell.SpatialFourierND.spatialAnnulusKernel_compact line 43
  6. theorem OAI.GraphLiteralSupport.Attempt4PrefixShell.SpatialFourierND.spatialAnnulusKernel_eq line 48
  7. def OAI.GraphLiteralSupport.Attempt4PrefixShell.SpatialFourierND.spatialAnnulusSchwartz line 57
  8. def OAI.GraphLiteralSupport.Attempt4PrefixShell.SpatialFourierND.spatialFourierCoeff line 76
  9. def OAI.GraphLiteralSupport.Attempt4PrefixShell.SpatialFourierND.spatialFourierCost line 79
  10. def OAI.GraphLiteralSupport.Attempt4PrefixShell.SpatialFourierND.spatialFourierPhase line 82
  11. theorem OAI.GraphLiteralSupport.Attempt4PrefixShell.SpatialFourierND.spatialFourierCost_nonneg line 85
  12. theorem OAI.GraphLiteralSupport.Attempt4PrefixShell.SpatialFourierND.spatialFourierPhase_continuous line 89
  13. theorem OAI.GraphLiteralSupport.Attempt4PrefixShell.SpatialFourierND.spatialFourierPhase_norm line 94
  14. theorem OAI.GraphLiteralSupport.Attempt4PrefixShell.SpatialFourierND.spatialFourierPhase_sub line 98
  15. theorem OAI.GraphLiteralSupport.Attempt4PrefixShell.SpatialFourierND.spatialFourierCoeff_integrable line 107
  16. theorem OAI.GraphLiteralSupport.Attempt4PrefixShell.SpatialFourierND.spatialFourierSeparation_integrable line 111
  17. theorem OAI.GraphLiteralSupport.Attempt4PrefixShell.SpatialFourierND.spatialFourierSeparation line 127
  18. theorem OAI.GraphLiteralSupport.Attempt4PrefixShell.SpatialFourierND.spatialInverseDistance_separation line 143
  19. def OAI.GraphLiteralSupport.Attempt4PrefixShell.SpatialFourierND.spatialPairPhase line 168
  20. theorem OAI.GraphLiteralSupport.Attempt4PrefixShell.SpatialFourierND.spatialPairPhase_continuous line 171
  21. theorem OAI.GraphLiteralSupport.Attempt4PrefixShell.SpatialFourierND.spatialPairPhase_norm line 176
  22. theorem OAI.GraphLiteralSupport.Attempt4PrefixShell.SpatialFourierND.spatialFourier_joint_integrable line 180
  23. theorem OAI.GraphLiteralSupport.Attempt4PrefixShell.SpatialFourierND.spatialFourier_integral_swap line 198