OAI/Analysis/LipschitzHilbert/Fourier/HilbertCutoffProfile.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The fixed smooth annular Hilbert multiplier and its cutoff derivative. All profiles are constructed, rather than supplied as analytic inputs.

  1. def OAI.LipschitzHilbert.PacketRepresentation.hilbertSmoothSign line 15
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.hilbertSmoothSign_smooth line 18
  3. theorem OAI.LipschitzHilbert.PacketRepresentation.hilbertSmoothSign_pos line 22
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.hilbertSmoothSign_neg line 26
  5. theorem OAI.LipschitzHilbert.PacketRepresentation.hilbertSmoothSign_range line 30
  6. theorem OAI.LipschitzHilbert.PacketRepresentation.hilbertSmoothSign_deriv_zero line 36
  7. theorem OAI.LipschitzHilbert.PacketRepresentation.verticalBinPlateauReal_smooth line 50
  8. theorem OAI.LipschitzHilbert.PacketRepresentation.verticalBinPlateauReal_range line 54
  9. theorem OAI.LipschitzHilbert.PacketRepresentation.verticalBinPlateauReal_one line 61
  10. theorem OAI.LipschitzHilbert.PacketRepresentation.verticalBinPlateauReal_deriv_zero line 66
  11. def OAI.LipschitzHilbert.PacketRepresentation.hilbertCutoffDerivative line 85
  12. def OAI.LipschitzHilbert.PacketRepresentation.hilbertAnnularSymbol line 100
  13. theorem OAI.LipschitzHilbert.PacketRepresentation.hilbertAnnularSymbol_support line 123