OAI/Analysis/LipschitzHilbert/Fourier/VerticalConvolutionL1.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Vertical convolution acts on actual measurable planar functions. Its L1 and uniform bounds are independent of bin width and carrier.

  1. def OAI.LipschitzHilbert.PacketRepresentation.verticalTranslation line 12
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.verticalTranslation_measurePreserving line 20
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.integral_verticalTranslation line 33
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.verticalConvolution_joint_integrable line 38
  5. theorem OAI.LipschitzHilbert.PacketRepresentation.verticalConvolution_measurable line 55
  6. theorem OAI.LipschitzHilbert.PacketRepresentation.verticalConvolution_integrable line 61
  7. theorem OAI.LipschitzHilbert.PacketRepresentation.verticalConvolution_l1_bound line 66
  8. theorem OAI.LipschitzHilbert.PacketRepresentation.verticalConvolution_horizontal_support line 82