OAI/Analysis/LipschitzHilbert/Estimates/TopMaskApproximation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The manuscript mask at its actual scale. Inside the prescribed near region its error is at most a fixed constant times L^(1-A).

  1. def OAI.LipschitzHilbert.topSincMask line 13
  2. theorem OAI.LipschitzHilbert.topSincMask_nonneg line 16
  3. theorem OAI.LipschitzHilbert.topSincMask_le_one line 19
  4. theorem OAI.LipschitzHilbert.topSincMask_error_le_one line 22
  5. theorem OAI.LipschitzHilbert.abs_one_sub_sincProductMask_scaled line 26
  6. theorem OAI.LipschitzHilbert.topSincMask_near_error line 40