OAI/Analysis/LipschitzHilbert/Fourier/VerticalBinKernel.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Exact modulated convolution kernels for the fixed vertical bin profiles, with a uniform L1 norm at every width and carrier.

  1. def OAI.LipschitzHilbert.PacketRepresentation.modulatedTimeKernel line 14
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.modulatedTimeKernel_integrable line 17
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.modulatedTimeKernel_fourier line 25
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.modulatedTimeKernel_norm line 36
  5. theorem OAI.LipschitzHilbert.PacketRepresentation.modulatedTimeKernel_l1 line 41
  6. def OAI.LipschitzHilbert.PacketRepresentation.verticalProfileKernel line 48
  7. theorem OAI.LipschitzHilbert.PacketRepresentation.verticalProfileKernel_fourier line 51
  8. def OAI.LipschitzHilbert.PacketRepresentation.verticalConvolution line 57
  9. theorem OAI.LipschitzHilbert.PacketRepresentation.verticalConvolution_uniform_bound line 60