OAI/Analysis/LipschitzHilbert/Fourier/GlobalBandOperator.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Global positive and negative vertical-band bounds at one absolute short scale, conditional on martingale variation, the directional maximal estimate, and the horizontal Hilbert estimate.

  1. def OAI.LipschitzHilbert.PacketRepresentation.sharpBandOperator line 14
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.sharpBandOperator_norm_of_strip_bounds line 21
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.global_positive_band_operator_norm line 32
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.global_negative_band_operator_norm line 43