OAI/Analysis/LipschitzHilbert/Fourier/AnnularBinPairing.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

On the original narrow horizontal strip, the actual projected time pairing equals the finite annular-symbol pairing without a time cutoff.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.annularBin_pairing line 14