OAI/Analysis/LipschitzHilbert/Fourier/SharpBandUniformHigh.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The source time/width choices and exponential absorption give the uniform high-disparity restricted estimate for every sharp truncation.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.actual_sharp_band_uniform_high line 13