OAI/Analysis/LipschitzHilbert/Fourier/PositiveLineKernel.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The positive horizontal convolution kernel used for the error majorant, with its short-interval integral bound.

  1. def OAI.LipschitzHilbert.lineKernel line 14
  2. theorem OAI.LipschitzHilbert.lineKernel_nonneg line 16
  3. theorem OAI.LipschitzHilbert.lineKernel_shift line 19
  4. theorem OAI.LipschitzHilbert.lineKernel_integrable line 23
  5. theorem OAI.LipschitzHilbert.integral_lineKernel_le line 28
  6. theorem OAI.LipschitzHilbert.local_lineKernel_integral line 37