OAI/Analysis/LipschitzHilbert/Fourier/SharpBandRestrictedLog.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The three actual sharp band regimes give the logarithmic restricted estimate on Schwartz tests, uniformly in the inner endpoint and width.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.log_mass_ratio line 14
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.actual_sharp_band_restricted_log line 20