OAI/Analysis/LipschitzHilbert/Fourier/ErrorLineConcentration.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Line moments of the positive error majorant, and transfer to any measurable nonnegative error that it dominates.

  1. theorem OAI.LipschitzHilbert.LineErrorSources.majorant_root_integral line 18
  2. theorem OAI.LipschitzHilbert.LineErrorSources.majorant_mean line 39
  3. theorem OAI.LipschitzHilbert.LineErrorSources.majorant_moment line 53
  4. theorem OAI.LipschitzHilbert.LineErrorSources.dominated_error_moment line 82