OAI/Analysis/LipschitzHilbert/Fourier/PositiveConvolution.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Actual convolution of the positive error source with the horizontal kernel. Bounded measurable sources need not be globally integrable.

  1. def OAI.LipschitzHilbert.positiveConvolution line 14
  2. theorem OAI.LipschitzHilbert.lineKernel_continuous line 17
  3. theorem OAI.LipschitzHilbert.lineKernel_sub_comm line 20
  4. theorem OAI.LipschitzHilbert.positiveConvolution_integrable_at line 23
  5. theorem OAI.LipschitzHilbert.positiveConvolution_nonneg line 31
  6. theorem OAI.LipschitzHilbert.positiveConvolution_le line 35
  7. theorem OAI.LipschitzHilbert.positiveConvolution_joint_integrable line 54
  8. theorem OAI.LipschitzHilbert.positiveConvolution_interval_integrable line 84
  9. theorem OAI.LipschitzHilbert.integral_positiveConvolution_interval line 90