OAI/MeasureTheory/FalconerCompletion/Fourier/QuadraticKernel.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Fourier kernels and oscillatory estimates.

  1. def OAI.GraphLiteralSupport.Attempt4FullFar.quadraticKernelND line 20
  2. lemma OAI.GraphLiteralSupport.Attempt4FullFar.fourier_quadraticGaussianND line 24
  3. lemma OAI.GraphLiteralSupport.Attempt4FullFar.quadraticGaussianND_pairing line 28
  4. lemma OAI.GraphLiteralSupport.Attempt4FullFar.quadratic_exponentialND_norm_le_one line 45
  5. lemma OAI.GraphLiteralSupport.Attempt4FullFar.quadraticKernelND_norm_le line 57
  6. lemma OAI.GraphLiteralSupport.Attempt4FullFar.quadraticKernelND_damped_bound line 76
  7. lemma OAI.GraphLiteralSupport.Attempt4FullFar.quadraticKernelND_continuous_damping line 85
  8. lemma OAI.GraphLiteralSupport.Attempt4FullFar.quadraticKernelND_integral_limit line 106
  9. lemma OAI.GraphLiteralSupport.Attempt4FullFar.quadraticGaussianND_integral_limit line 124
  10. lemma OAI.GraphLiteralSupport.Attempt4FullFar.quadratic_oscillatoryND_pairing line 148
  11. def OAI.GraphLiteralSupport.Attempt4FullFar.fresnelCoefficientND line 161
  12. lemma OAI.GraphLiteralSupport.Attempt4FullFar.quadraticND_fresnel_coefficient line 167
  13. lemma OAI.GraphLiteralSupport.Attempt4FullFar.fresnelCoefficientND_norm line 188
  14. theorem OAI.GraphLiteralSupport.Attempt4FullFar.quadratic_stationaryND_identity line 193