OAI/Analysis/LipschitzHilbert/Fourier/UnitConvolutionParameter.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Joint dependence on the remaining Fourier parameter. These are the literal kernels and selectors in the packet representation, so their finite sums may be integrated against the outside symbol weight.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.symbolWeight_continuous line 14
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.unitPacketSelector_joint_continuous line 19
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.frequencyKernel_convolution line 34
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.frequencyKernel_convolution_joint_continuous line 49
  5. theorem OAI.LipschitzHilbert.PacketRepresentation.unitConvolution_pairing_stronglyMeasurable line 58