OAI/Analysis/LipschitzHilbert/Fourier/L1FourierConvolution.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Fourier multiplication by a Schwartz kernel is convolution for every L1 input. This includes the measurable amplitude slices used after binning.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.planarFourier_l1_bound line 12
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.planarFourier_l1_continuous line 19
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.planarInverse_mul_fourier_l1 line 32