OAI/Analysis/LipschitzHilbert/Estimates/DyadicLongScales.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The reciprocal lengths of the scales longer than an interval form a geometric sum controlled by that interval's reciprocal length.

  1. theorem OAI.LipschitzHilbert.sum_two_powers line 14
  2. theorem OAI.LipschitzHilbert.sum_long_dyadic_reciprocals line 20