OAI/Analysis/LipschitzHilbert/Fourier/SchwartzVerticalProjection.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Vertical frequency cutoffs preserve the actual planar Schwartz class.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.verticalProfile_temperate line 11
  2. def OAI.LipschitzHilbert.PacketRepresentation.schwartzVerticalProjection line 17
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.schwartzVerticalProjection_fourier line 22
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.schwartzVerticalProjection_eq_convolution line 30
  5. theorem OAI.LipschitzHilbert.PacketRepresentation.planar_schwartz_ext_fourier line 43