OAI/Analysis/LipschitzHilbert/Fourier/FrequencyKernelTranslations.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Fourier characters translate the actual convolution kernels. Their translation vectors follow the packet's long and short coordinates.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.planarInverse_modulatedFrequencyWindow line 13
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.planarInverseSchwartz_smul line 28
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.horizontalFrequencyKernel_apply line 33
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.verticalFrequencyKernel_apply line 42