OAI/Analysis/LipschitzHilbert/Fourier/VerticalErrorSources.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Averaging the error sources with the common vertical kernel preserves the pointwise and summed bounds used on every reference line.

  1. theorem OAI.LipschitzHilbert.positiveConvolution_finset_sum line 14
  2. theorem OAI.LipschitzHilbert.verticalConvolution_measurable line 22
  3. def OAI.LipschitzHilbert.verticalErrorSources line 28