OAI/Analysis/LipschitzHilbert/Fourier/LineProductSpectrum.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The Fourier spectrum of an actual Schwartz product, including the ball and annulus bounds needed in the dyadic commutator decomposition.

  1. def OAI.LipschitzHilbert.PacketRepresentation.lineSchwartzProduct line 12
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.lineSchwartzProduct_apply line 15
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.schwartz_fourier_twice line 19
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.lineSchwartzProduct_fourier line 26
  5. theorem OAI.LipschitzHilbert.PacketRepresentation.lineSchwartzProduct_fourier_zero line 40
  6. theorem OAI.LipschitzHilbert.PacketRepresentation.lineSchwartzProduct_band line 49
  7. theorem OAI.LipschitzHilbert.PacketRepresentation.lineSchwartzProduct_annular_lower line 65