OAI/Analysis/LipschitzHilbert/Trees/SourceResidualMask.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The mask in §4 is dominated by the actual hierarchy weight with dilation L^(A+2). Consequently the negative weight power in every residual coefficient costs at most one, uniformly in the spatial point.

  1. theorem OAI.LipschitzHilbert.topSincMask_abs_le_one line 12
  2. theorem OAI.LipschitzHilbert.topSincMask_radial_power line 16
  3. theorem OAI.LipschitzHilbert.topSincMask_le_topShape line 62
  4. theorem OAI.LipschitzHilbert.negative_weight_power_mul_le_one line 98
  5. theorem OAI.LipschitzHilbert.SlopeBox.residual_mask_weight_bound line 111