OAI/Analysis/LipschitzHilbert/Fourier/AnnularPVFromNarrow.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A fixed finite frequency covering converts the narrow-band hypothesis into uniform bounds for all dilated annular inputs.

  1. def OAI.LipschitzHilbert.PacketRepresentation.fixedAnnulus line 13
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.fixedAnnulus_compact line 15
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.exists_annular_PV_constant line 22
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.annularProjection_fourier_support line 44
  5. theorem OAI.LipschitzHilbert.PacketRepresentation.reassemblyDifference_fixedAnnulus line 52