OAI/Analysis/LipschitzHilbert/Fourier/AnnularBinMultiplier.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The annular symbol with the enlarged bin plateau is exactly the time kernel acting on the true bin projection.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.annularBinMultiplier_eq line 14
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.slopeKernelOperator_finiteTimeKernel line 35