OAI/Analysis/LipschitzHilbert/Fourier/LocalizedBandOperator.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The localized positive-band Hilbert operator has a uniform L2 norm, independent of its sharp inner endpoint and vertical frequency width.

  1. def OAI.LipschitzHilbert.PacketRepresentation.localizedSharpBandOperator line 12
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.localizedSharpBandPairing_eq_inner line 20
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.localized_sharp_band_operator_norm line 30