OAI/Analysis/LipschitzHilbert/Trees/SourceMaskTail.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The source sinc mask is exponentially small outside the prescribed polynomial enlargement of its top. The estimate includes points on either coordinate axis and uses the actual even exponent 2 * ceil L.

  1. theorem OAI.LipschitzHilbert.abs_sinc_le_reciprocal_of_large line 12
  2. theorem OAI.LipschitzHilbert.sincProductMask_tail line 20
  3. theorem OAI.LipschitzHilbert.topSincMask_tail line 50
  4. theorem OAI.LipschitzHilbert.SlopeBox.mask_tail line 71