OAI/Analysis/LipschitzHilbert/Trees/SourceThresholdSum.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Uniform summation over any finite family of dyadic density thresholds.

  1. def OAI.LipschitzHilbert.ordinaryThresholdRatio line 12
  2. def OAI.LipschitzHilbert.ordinaryThresholdEnvelope line 14
  3. theorem OAI.LipschitzHilbert.ordinaryThresholdRatio_pos line 16
  4. theorem OAI.LipschitzHilbert.ordinaryThresholdRatio_lt_one line 19
  5. theorem OAI.LipschitzHilbert.ordinaryThresholdEnvelope_summable line 22
  6. theorem OAI.LipschitzHilbert.ordinaryThresholdEnvelope_tsum line 31
  7. theorem OAI.LipschitzHilbert.ordinaryThresholdWeight_dyadic line 50
  8. theorem OAI.LipschitzHilbert.ordinaryThreshold_finite_sum line 77
  9. theorem OAI.LipschitzHilbert.ordinaryThresholdWeight_scale_upper line 93
  10. theorem OAI.LipschitzHilbert.ordinaryThreshold_finite_sum_bounded line 107