OAI/Analysis/LipschitzHilbert/Trees/SourceOffchildMask.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A loss below one contains only tops outside their weight dilation. Their actual sinc masks are exponentially small, so the off-child error is paid by the exact lost mass.

  1. theorem OAI.LipschitzHilbert.SlopeBox.one_le_weight_of_radius_le line 14
  2. theorem OAI.LipschitzHilbert.SlopeBox.radius_large_of_weight_lt_one line 31
  3. theorem OAI.LipschitzHilbert.AngularGrid.source_offchild_weight_lt_one line 41
  4. theorem OAI.LipschitzHilbert.AngularGrid.source_offchild_masked_amplitude_bound line 70