OAI/Analysis/LipschitzHilbert/Estimates/PrincipalValueProfileCommutator.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

An unconditional L2 estimate for the actual principal-value/profile commutator on a vertically band-limited input. It includes the passage to the singular kernel, rather than assuming a bounded full PV operator.

  1. theorem OAI.LipschitzHilbert.PacketRepresentation.sharpVerticalCommutator_bound line 13
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.principalValueProfileCommutator_measurable line 34
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.principalValueProfileCommutator_bound line 43