OAI/Analysis/LipschitzHilbert/Packets/PlanarFrequencyPackets.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The two separated frequency factors are Fourier transforms of actual Schwartz convolution kernels. Thus the lattice average uses actual packets.

  1. def OAI.LipschitzHilbert.PacketRepresentation.planarInverseSchwartz line 13
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.planarInverseSchwartz_fourier line 16
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.planarInverseSchwartz_apply line 21
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.affineFrequencyCharacter_temperate line 28
  5. def OAI.LipschitzHilbert.PacketRepresentation.modulatedFrequencyWindow line 37
  6. theorem OAI.LipschitzHilbert.PacketRepresentation.modulatedFrequencyWindow_apply line 42
  7. def OAI.LipschitzHilbert.PacketRepresentation.horizontalFrequencyKernel line 48
  8. def OAI.LipschitzHilbert.PacketRepresentation.verticalFrequencyKernel line 53
  9. theorem OAI.LipschitzHilbert.PacketRepresentation.frequencyKernel_product line 58
  10. theorem OAI.LipschitzHilbert.PacketRepresentation.frequencyKernel_packet_average line 75