OAI/Analysis/LipschitzHilbert/Fourier/LineKernelOscillation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

An integrable pointwise majorant for translations of a long-scale kernel. It is used before integrating against a bounded source.

  1. theorem OAI.LipschitzHilbert.lineEnvelope_nearby line 14
  2. theorem OAI.LipschitzHilbert.lineKernel_shift_hasDerivAt line 30
  3. theorem OAI.LipschitzHilbert.lineKernel_shift_derivative_bound line 38
  4. theorem OAI.LipschitzHilbert.lineKernel_translation_bound line 52