OAI/Analysis/LipschitzHilbert/Fourier/LineKernelScaling.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual line projection kernel has the expected physical scale, including its exact first absolute moment.

  1. def OAI.LipschitzHilbert.PacketRepresentation.scaledSchwartzKernel line 13
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.scaledSchwartzKernel_apply line 16
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.lineProjectionKernel_eq_scaled line 22
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.lineProjectionKernel_moment1 line 35