OAI/Analysis/LipschitzHilbert/Fourier/VerticalConvolutionLp.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Vertical convolution on the L2 quotient, with its actual integral representative.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.verticalConvolution_congr_ae line 11
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.verticalConvolution_integrand_ae line 27
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.verticalConvolution_sub_ae line 39
  4. def OAI.LipschitzHilbert.PacketRepresentation.verticalConvolutionLp line 50
  5. theorem OAI.LipschitzHilbert.PacketRepresentation.verticalConvolutionLp_coe line 55
  6. theorem OAI.LipschitzHilbert.PacketRepresentation.verticalConvolutionLp_toLp line 60
  7. theorem OAI.LipschitzHilbert.PacketRepresentation.verticalConvolutionLp_sub line 69
  8. theorem OAI.LipschitzHilbert.PacketRepresentation.verticalConvolutionLp_norm line 86
  9. theorem OAI.LipschitzHilbert.PacketRepresentation.verticalConvolutionLp_continuous line 98