OAI/Analysis/LipschitzHilbert/Estimates/SlopeMaskIntegral.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual sinc-masked slope-box synthesis on a finite testing measure. The amplitude bound is required only almost everywhere on that measure, allowing restriction to the good testing set.

  1. theorem OAI.LipschitzHilbert.exists_slope_mask_integral line 16
  2. theorem OAI.LipschitzHilbert.exists_slope_mask_integral_above line 43