OAI/Analysis/LipschitzHilbert/Fourier/LineLowHighSpectrum.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The low/high commutator output stays in a fixed annulus.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.lineSchwartzProjection_comm line 10
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.lowHighCommutator_frequency line 21