OAI/Analysis/LipschitzHilbert/Fourier/BoundedVerticalMultiplier.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The multiplier is linear in its Schwartz symbol on bounded measurable inputs. The input need not have finite L2 norm.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.lineProjectionKernel_add line 13
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.lineProjectionKernel_smul line 17
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.lineProjectionKernel_dilate line 21
  4. def OAI.LipschitzHilbert.PacketRepresentation.boundedVerticalMultiplierLM line 31
  5. theorem OAI.LipschitzHilbert.PacketRepresentation.boundedVerticalMultiplierLM_apply line 54
  6. theorem OAI.LipschitzHilbert.PacketRepresentation.verticalMultiplier_dilate line 59