OAI/Analysis/LipschitzHilbert/Fourier/VerticalCommutatorAverage.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A first-moment bound for the actual bin/sampling commutator, integrated over the short times allowed by the horizontal localization.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.verticalSamplingCommutator_joint_measurable line 12
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.verticalProfileCommutator_average_energy line 29