OAI/Analysis/LipschitzHilbert/Fourier/LocalizedBandStrong.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Uniform strong L2 control of the actual positive-band pairing, localized in a narrow horizontal strip.

  1. def OAI.LipschitzHilbert.PacketRepresentation.horizontalStrip line 14
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.horizontalStrip_measurable line 16
  3. def OAI.LipschitzHilbert.PacketRepresentation.stripL2Cutoff line 19
  4. def OAI.LipschitzHilbert.PacketRepresentation.localizedSharpBandPairing line 22
  5. theorem OAI.LipschitzHilbert.PacketRepresentation.indicator_unit line 28
  6. theorem OAI.LipschitzHilbert.PacketRepresentation.indicator_support_subset line 35
  7. theorem OAI.LipschitzHilbert.PacketRepresentation.localized_sharp_band_strong line 43