OAI/Analysis/LipschitzHilbert/Fourier/ActualBandHigh.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The high-disparity bound for the localized finite time operator, combining the diagonal bin estimate and the full commutator error under the martingale variation and directional maximal hypotheses.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.actual_band_high line 15