OAI/Analysis/LipschitzHilbert/Fourier/SharpKernelComparison.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The two endpoint envelopes control sharp truncation versus a telescoped kernel. The profile conditions are local construction obligations.

  1. def OAI.LipschitzHilbert.PacketRepresentation.sharpTimeKernel line 12
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.profile_far_bound line 15
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.sharpKernelComparison_pointwise line 23
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.sharpTimeKernel_measurable line 109
  5. theorem OAI.LipschitzHilbert.PacketRepresentation.sharpKernelComparison_integral line 113
  6. theorem OAI.LipschitzHilbert.PacketRepresentation.finiteTimeKernel_sharp_integral line 137