OAI/Analysis/LipschitzHilbert/Fourier/VerticalKernelMoment.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The second absolute moment of a modulated bin kernel has exactly the square of its physical width. The carrier does not affect it.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.schwartz_second_absolute_moment_integrable line 11
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.modulatedTimeKernel_moment2_pointwise line 15
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.modulatedTimeKernel_moment2_integrable line 20
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.modulatedTimeKernel_moment2 line 27