OAI/Analysis/LipschitzHilbert/Estimates/MaskComparison.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Quantitative comparison of a finite top synthesis with its actual sinc-masked version. The near and far estimates use the same fixed polynomial top envelope.

  1. theorem OAI.LipschitzHilbert.norm_sum_sub_mask_le line 15
  2. theorem OAI.LipschitzHilbert.topSincMask_near_far line 36