OAI/MeasureTheory/FalconerCompletion/Fourier/SchwartzNormMonomialIntegrable2.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Fourier kernels and oscillatory estimates.

  1. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.schwartz_norm_monomialND_integrable line 20
  2. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.imaginaryTaylor_quadraticND_eq line 27
  3. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.imaginaryTaylor_quadraticND_integrable line 39
  4. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.imaginaryExponential_quadraticND_integrable line 46
  5. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.quadraticND_taylor_integral_bound line 54
  6. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.imaginaryTaylor_quadraticND_integral line 70
  7. def OAI.GraphLiteralSupport.Attempt4PrefixShell.quadraticExpansionND line 81
  8. theorem OAI.GraphLiteralSupport.Attempt4PrefixShell.quadratic_stationaryND_expansion line 86
  9. def OAI.GraphLiteralSupport.Attempt4PrefixShell.fourierDerivativeND_L1 line 118
  10. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.fourierDerivativeND_L1_nonneg line 121
  11. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.schwartz_fourierND_weighted_pointwise line 126
  12. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.schwartz_fourierND_weighted_decay line 135
  13. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.schwartz_fourierND_moment_bound line 157
  14. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.schwartz_inverseND_moment_bound line 171
  15. theorem OAI.GraphLiteralSupport.Attempt4PrefixShell.quadratic_stationaryND_expansion_L1 line 183
  16. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.schwartz_fourierInv_laplacianND line 210
  17. def OAI.GraphLiteralSupport.Attempt4PrefixShell.iteratedLaplacianND line 232
  18. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.schwartz_fourierInv_iteratedLaplacianND line 236
  19. lemma OAI.GraphLiteralSupport.Attempt4PrefixShell.schwartz_inverseND_even_moment line 246
  20. theorem OAI.GraphLiteralSupport.Attempt4PrefixShell.quadraticExpansionND_eq_local line 262