OAI/Analysis/LipschitzHilbert/Fourier/BandAmplitudeError.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual diagonal form changes by a controlled amount when all logarithmically discarded amplitude levels are removed.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.band_diagonal_amplitude_error line 15