OAI/Analysis/LipschitzHilbert/Estimates/PrincipalTimeMoment.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The principal-value kernel is not absolutely integrable, but its first absolute moment is. This is the cancellation needed by the band-reassembly commutator, without assuming any Hilbert-transform estimate.

  1. def OAI.LipschitzHilbert.PacketRepresentation.principalTimeKernel line 12
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.principalTimeKernel_measurable line 14
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.principalTimeKernel_first_moment line 17