OAI/Analysis/LipschitzHilbert/Fourier/DyadicCommutatorCutoff.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A fixed enlarged annulus for the low/high part of the commutator. Its support fits the already proved localized Mihlin kernel estimates.

  1. def OAI.LipschitzHilbert.PacketRepresentation.dyadicCommutatorCutoff line 11
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.dyadicCommutatorCutoff_apply line 15
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.dyadicCommutatorCutoff_one line 19
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.dyadicCommutatorCutoff_small line 25
  5. theorem OAI.LipschitzHilbert.PacketRepresentation.dyadicCommutatorCutoff_large line 31
  6. theorem OAI.LipschitzHilbert.PacketRepresentation.dyadicCommutatorCutoff_tsupport line 37
  7. theorem OAI.LipschitzHilbert.PacketRepresentation.dyadicCommutatorCutoff_away_zero line 45
  8. theorem OAI.LipschitzHilbert.PacketRepresentation.dyadicCommutatorCutoff_bounded_support line 49