OAI/Analysis/LipschitzHilbert/Packets/ConvolutionPacketProfile.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Normalized Schwartz profiles for the actual convolution packets, with arbitrary prescribed vertical carrier.

  1. def OAI.LipschitzHilbert.PacketRepresentation.convolutionProfile line 11
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.convolutionProfile_apply line 16
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.physical_convolution_packet line 25