OAI/MeasureTheory/FalconerCompletion/Fourier/SchwartzNormMonomialIntegrable.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

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