OAI/Analysis/LipschitzHilbert/Fourier/BoundedConvolutionL2.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

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

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.toL2_norm_le_of_integral line 13
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.lineConvolution_L2_norm_bound line 21
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.boundedConvolution_L2_difference line 28
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.boundedConvolution_L2_of_schwartz line 41