OAI/Analysis/LipschitzHilbert/Estimates/SlopeBoxMask.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The sinc mask in the manuscript's actual slope coordinates, with parameters fixed uniformly before choosing the finite top family.

  1. def OAI.LipschitzHilbert.SlopeBox.mask line 15
  2. theorem OAI.LipschitzHilbert.SlopeBox.weight_eq_topShape line 18
  3. theorem OAI.LipschitzHilbert.SlopeBox.mask_continuous line 21
  4. theorem OAI.LipschitzHilbert.SlopeBox.weight_continuous line 30
  5. theorem OAI.LipschitzHilbert.exists_uniform_top_mask_error line 43