OAI/Analysis/LipschitzHilbert/Fourier/AnnularPVPartialBound.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The finite annular output has a uniform L2 bound, derived directly from the annular input estimates and actual signed PV commutators.

  1. def OAI.LipschitzHilbert.PacketRepresentation.annularPVBoundConstant line 15
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.annularPVComm_eq line 18
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.annularPVPartial_bound line 29