OAI/NumberTheory/CubicMoment/Estimates/DyadicLittleO.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Summing a dyadic little-oh estimate at the Patterson scale. The local growth and the vanishing at small arguments are retained explicitly.

  1. lemma OAI.CubicFirstMoment.dyadicDifference_regularized_bound line 13
  2. theorem OAI.CubicFirstMoment.dyadic_littleO_firstMoment line 56