OAI/Analysis/LipschitzHilbert/Packets/FactoredMultiplierPackets.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A factored frequency multiplier is exactly the normalized average of its actual analyzing and synthesizing convolution packets.

  1. def OAI.LipschitzHilbert.lowerHilbertPlanarSchwartz line 14
  2. theorem OAI.LipschitzHilbert.hilbertPlanar_lower line 19
  3. def OAI.LipschitzHilbert.planarSchwartzConvolution line 24
  4. theorem OAI.LipschitzHilbert.planarSchwartzConvolution_apply line 28
  5. theorem OAI.LipschitzHilbert.planarFourier_convolution line 35
  6. theorem OAI.LipschitzHilbert.PacketRepresentation.factored_multiplier_convolution line 45
  7. theorem OAI.LipschitzHilbert.PacketRepresentation.factored_multiplier_packet_average line 55