OAI/Analysis/LipschitzHilbert/Fourier/LineBandedCommutatorEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Removing coefficient smoothing gives the uniform commutator bound for every finite collection of actual input frequency bands.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.lineBandedCommutator_energy line 13