OAI/Analysis/LipschitzHilbert/Fourier/FourierKernelFirstMoment.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A quantitative first absolute moment from the zeroth and third L1 derivatives of a Schwartz multiplier.

  1. def OAI.LipschitzHilbert.PacketRepresentation.schwartzDerivative line 13
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.schwartzDerivative_apply line 17
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.fourier_schwartzDerivative line 26
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.schwartz_fourier_norm_le_l1 line 40
  5. theorem OAI.LipschitzHilbert.PacketRepresentation.schwartz_fourier_weighted_norm line 45
  6. theorem OAI.LipschitzHilbert.PacketRepresentation.firstMoment_bound_of_decay line 55
  7. theorem OAI.LipschitzHilbert.PacketRepresentation.schwartz_fourier_firstMoment_bound line 91