OAI/NumberTheory/CubicMoment/Decomposition/StoppedMellinScale.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Rounding the coefficient length in the ordinary mean introduces only fixed factors. Its logarithmic cutoff remains a fixed power of log X.

  1. lemma OAI.CubicFirstMoment.stopped_mellin_ceil_scale line 10
  2. lemma OAI.CubicFirstMoment.stopped_mellin_cutoff_scale line 30
  3. lemma OAI.CubicFirstMoment.stopped_mellin_mass_scale line 39