OAI/Analysis/LipschitzHilbert/Estimates/MeasureClassLog.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The logarithmic restricted estimate is dominated by the summable kernel of the actual dyadic support-measure classes.

  1. def OAI.LipschitzHilbert.measureClassLogConstant line 11
  2. theorem OAI.LipschitzHilbert.measure_class_log_bound line 13