OAI/Analysis/LipschitzHilbert/Estimates/PolynomialLocalization.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

The positive polynomial weights used to localize annular packets on a reference line. Their construction and Fourier support preservation are proved here for the actual Schwartz functions.

  1. theorem OAI.LipschitzHilbert.fourier_support_add_subset line 16
  2. theorem OAI.LipschitzHilbert.fourier_support_smul_subset line 32
  3. def OAI.LipschitzHilbert.centeredCoordinateProduct line 38
  4. theorem OAI.LipschitzHilbert.centeredCoordinateProduct_apply line 41
  5. theorem OAI.LipschitzHilbert.centeredCoordinateProduct_fourier_support line 47
  6. def OAI.LipschitzHilbert.quadraticLocalization line 53
  7. theorem OAI.LipschitzHilbert.quadraticLocalization_apply line 56
  8. theorem OAI.LipschitzHilbert.quadraticLocalization_fourier_support line 63
  9. def OAI.LipschitzHilbert.polynomialWeight line 71
  10. def OAI.LipschitzHilbert.polynomialLocalization line 74
  11. theorem OAI.LipschitzHilbert.polynomialLocalization_apply line 78
  12. theorem OAI.LipschitzHilbert.polynomialWeight_one_le line 88
  13. theorem OAI.LipschitzHilbert.polynomialLocalization_fourier_support line 95
  14. theorem OAI.LipschitzHilbert.fourier_support_annulus line 103
  15. theorem OAI.LipschitzHilbert.polynomialLocalization_low line 115
  16. theorem OAI.LipschitzHilbert.polynomialLocalization_high line 124