OAI/Analysis/LipschitzHilbert/Fourier/ActualCutoffBandHigh.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The actual high-disparity estimate with the original band cutoff on the input. The original bounded input need not itself have a spectrum.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.slopeKernelOperator_schwartz_smul line 13
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.bandProjection_pairing_normalize line 23
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.actual_cutoff_band_high line 37