OAI/NumberTheory/CubicMoment/Estimates/DivisorTailScale.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A small square divisor leaves a positive-power gap beyond the effective-frequency cutoff.

  1. lemma OAI.CubicFirstMoment.divisor_tail_lower_scale line 10
  2. lemma OAI.CubicFirstMoment.divisor_tail_upper_scale line 26