OAI/Analysis/LipschitzHilbert/Fourier/BoundedConvolutionL4.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Transfer of a Schwartz L4 convolution bound to bounded measurable L4 inputs, using density and the actual convolution difference.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.toL4_norm_le_of_integral line 13
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.lineConvolution_L4_norm_bound line 21
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.lineConvolution_L4_difference line 28
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.boundedConvolution_L4_of_schwartz line 41