OAI/NumberTheory/CubicMoment/Estimates/DyadicScaleBounds.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A summable majorant for first-moment scales along contracting dyads.

  1. def OAI.CubicFirstMoment.regularizedMomentScale line 11
  2. def OAI.CubicFirstMoment.dyadicMomentRatio line 13
  3. lemma OAI.CubicFirstMoment.regularizedMomentScale_pos line 16
  4. lemma OAI.CubicFirstMoment.regularized_dyadic_scale line 22
  5. lemma OAI.CubicFirstMoment.dyadicMomentRatio_summable line 50
  6. lemma OAI.CubicFirstMoment.firstMomentScale_le_two_regularized line 64
  7. lemma OAI.CubicFirstMoment.firstMomentScale_dyadic_isBigO line 73