OAI/Analysis/LipschitzHilbert/Trees/SourceWeightPointwiseBudget.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Elementary pointwise consequences of the actual top weights and the polynomial count cutoff. They supply the uniform weight and logarithmic mass bounds used in central interpolation and boundary averaging.

  1. theorem OAI.LipschitzHilbert.SlopeBox.weight_le_two_rpow line 14
  2. theorem OAI.LipschitzHilbert.SlopeBox.weight_mono_dilation line 22
  3. theorem OAI.LipschitzHilbert.eventually_count_log_bound line 33