OAI/Analysis/LipschitzHilbert/Fourier/AnnularPVCommutatorSquare.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The signed commutator estimate controls the square sum of individual actual annular PV commutators without assuming a full PV L2 operator.

  1. def OAI.LipschitzHilbert.PacketRepresentation.annularProfile line 14
  2. def OAI.LipschitzHilbert.PacketRepresentation.annularPVComm line 18
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.signedAnnularSymbol_fin line 22
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.annularPVComm_signed line 32
  5. theorem OAI.LipschitzHilbert.PacketRepresentation.annularPVComm_square line 45