OAI/Analysis/LipschitzHilbert/Estimates/LocalizedMihlinProfile.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Uniform derivative bounds for a rescaled multiplier after restriction to a fixed annulus. These are the bounds needed for its kernel moment.

  1. def OAI.LipschitzHilbert.PacketRepresentation.localizedMihlinProfile line 12
  2. theorem OAI.LipschitzHilbert.PacketRepresentation.localizedMihlinProfile_apply line 16
  3. def OAI.LipschitzHilbert.PacketRepresentation.annularDerivativeBudget line 22
  4. theorem OAI.LipschitzHilbert.PacketRepresentation.annularDerivativeBudget_nonneg line 25
  5. theorem OAI.LipschitzHilbert.PacketRepresentation.dilated_mihlin_derivative_bound line 29
  6. theorem OAI.LipschitzHilbert.PacketRepresentation.localizedMihlinProfile_derivative_bound line 45
  7. theorem OAI.LipschitzHilbert.PacketRepresentation.schwartz_l1_bound_of_support line 77
  8. theorem OAI.LipschitzHilbert.PacketRepresentation.schwartzDerivative_l1_bound_of_support line 91
  9. theorem OAI.LipschitzHilbert.PacketRepresentation.localizedMihlinProfile_tsupport line 100
  10. theorem OAI.LipschitzHilbert.PacketRepresentation.localizedMihlinProfile_l1 line 109
  11. def OAI.LipschitzHilbert.PacketRepresentation.localizedKernelFirstMomentConstant line 121
  12. theorem OAI.LipschitzHilbert.PacketRepresentation.localizedKernelFirstMomentConstant_nonneg line 125
  13. theorem OAI.LipschitzHilbert.PacketRepresentation.localizedMihlinProfile_fourier_firstMoment line 132
  14. theorem OAI.LipschitzHilbert.PacketRepresentation.schwartz_fourierInv_firstMoment_eq line 153
  15. theorem OAI.LipschitzHilbert.PacketRepresentation.localizedMihlinProfile_kernel_firstMoment line 170