OAI/Analysis/LipschitzHilbert/Fourier/ConvolutionBasicL1.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Integrability and a uniform pointwise bound for convolution of an integrable kernel with a Schwartz function.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.lineConvolution_integrable line 11
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.lineConvolution_bound line 17

    Distinct definitions of this name: OAI/Analysis/LipschitzHilbert/Fourier/LineConvolutionLocal.lean:10 (different declaration text). Qualify references as OAI.LipschitzHilbert.PacketRepresentation.lineConvolution_bound@path.