OAI/Analysis/LipschitzHilbert/Fourier/ScalarBandKernel.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The scalar annular form is the actual time operator applied to the original vertical cutoff; the test is not projected.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.annularScalarMultiplier_eq line 13
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.scalarBandForm_eq_kernel line 33