OAI/Analysis/LipschitzHilbert/Fourier/CoordinateFourierSupport.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Multiplication by the line coordinate preserves Fourier support for Schwartz functions. This is the first step in polynomial localization of the annular packet variation estimate.

  1. def OAI.LipschitzHilbert.coordinateProduct line 17
  2. theorem OAI.LipschitzHilbert.coordinateProduct_apply line 20
  3. theorem OAI.LipschitzHilbert.fourier_coordinate_derivative line 25
  4. theorem OAI.LipschitzHilbert.coordinateProduct_fourier_support line 44