OAI/Analysis/LipschitzHilbert/Estimates/SharpTimeMoment.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A sharply truncated Hilbert kernel has first absolute moment at most twice its outer radius, independently of the inner truncation.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.sharpTimeKernel_first_moment line 11
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.sharpTimeKernel_integrable line 44