OAI/Analysis/LipschitzHilbert/Fourier/SharpVerticalCommutator.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The actual vertical-profile commutator has a bound independent of the inner cutoff. Its principal-time integral has the same bound.

  1. def OAI.LipschitzHilbert.PacketRepresentation.sharpVerticalCommutator line 14
  2. def OAI.LipschitzHilbert.PacketRepresentation.principalVerticalCommutator line 21
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.profileTimeCommutator_energy line 26
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.sharpVerticalCommutator_eq line 48
  5. theorem OAI.LipschitzHilbert.PacketRepresentation.sharpVerticalCommutator_energy line 64
  6. theorem OAI.LipschitzHilbert.PacketRepresentation.principalVerticalCommutator_energy line 77