OAI/Analysis/LipschitzHilbert/Fourier/AnnularSelector.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

A fixed smooth annular selector. Multiplying the separated selector by this cutoff gives the required support away from the reference slope.

  1. def OAI.LipschitzHilbert.PacketRepresentation.selectorInner line 11
  2. def OAI.LipschitzHilbert.PacketRepresentation.selectorOuter line 14
  3. def OAI.LipschitzHilbert.PacketRepresentation.annularCutoff line 17
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.annularCutoff_apply line 23
  5. theorem OAI.LipschitzHilbert.PacketRepresentation.annularCutoff_nonneg line 26
  6. theorem OAI.LipschitzHilbert.PacketRepresentation.annularCutoff_le_one line 30
  7. theorem OAI.LipschitzHilbert.PacketRepresentation.annularCutoff_one line 39
  8. theorem OAI.LipschitzHilbert.PacketRepresentation.annularCutoff_support line 48
  9. def OAI.LipschitzHilbert.PacketRepresentation.localizedSelector line 64
  10. theorem OAI.LipschitzHilbert.PacketRepresentation.localizedSelector_bound line 68
  11. theorem OAI.LipschitzHilbert.PacketRepresentation.localizedSelector_support line 75