OAI/Analysis/LipschitzHilbert/Fourier/LineCommutatorEnergy.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The L2 kernel commutator estimate for multiplication by a bounded Lipschitz function. The cost is its Lipschitz bound times the first moment.

  1. def OAI.LipschitzHilbert.PacketRepresentation.lineMultiplicationCommutator line 12
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.lineMoment_dominated_energy line 15
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.lineMultiplicationCommutator_formula line 54
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.lineMultiplicationCommutator_energy line 69