OAI/Analysis/LipschitzHilbert/Trees/SourceReverseWeights.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Numerical weights for the bounded-input, unequal-measure estimate.

  1. def OAI.LipschitzHilbert.reverseThresholdWeight line 10
  2. def OAI.LipschitzHilbert.reverseThresholdRatio line 13
  3. theorem OAI.LipschitzHilbert.reverseThresholdRatio_pos line 15
  4. theorem OAI.LipschitzHilbert.reverseThresholdRatio_lt_one line 18
  5. theorem OAI.LipschitzHilbert.reverse_density_factor line 21
  6. theorem OAI.LipschitzHilbert.reverseThresholdWeight_le_shape line 36
  7. theorem OAI.LipschitzHilbert.reverse_shape_small line 43
  8. theorem OAI.LipschitzHilbert.reverse_shape_dyadic line 53
  9. theorem OAI.LipschitzHilbert.reverse_scale_power_le line 74
  10. theorem OAI.LipschitzHilbert.reverseThresholdWeight_scale line 91
  11. theorem OAI.LipschitzHilbert.reverseThreshold_dyadic_majorant line 113
  12. theorem OAI.LipschitzHilbert.reverseThreshold_finite_sum line 132