OAI/Analysis/LipschitzHilbert/Fourier/SharpBandHigh.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The high-disparity packet theorem now bounds the actual sharp Hilbert truncation, with its three explicit analytic remainder terms.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.dyadic_time_lower line 12
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.actual_sharp_band_high line 19