OAI/Analysis/LipschitzHilbert/Fourier/LineConvolutionLocal.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Bounded line convolutions have finite local square energy.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.lineConvolution_bound line 10

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

  2. theorem OAI.LipschitzHilbert.PacketRepresentation.lineConvolution_integrableOn_sq line 19