OAI/Analysis/LipschitzHilbert/Trees/SourceThresholdWeights.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The numerical density-size weight has summable decay on both sides of the unit scale, with the quarter-power density gain.

  1. def OAI.LipschitzHilbert.ordinaryThresholdWeight line 10
  2. theorem OAI.LipschitzHilbert.min_le_quarter_interpolation line 13
  3. theorem OAI.LipschitzHilbert.ordinaryThresholdWeight_nonneg line 33
  4. theorem OAI.LipschitzHilbert.ordinaryThresholdWeight_small line 38
  5. theorem OAI.LipschitzHilbert.ordinaryThresholdWeight_large line 68