OAI/NumberTheory/CubicMoment/Decomposition/StoppedCoreScale.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Scalar logarithmic absorption for the pointwise stopped-core sieve. The power saving is measured at the coefficient length; its comparison with the outer length is retained explicitly.

  1. lemma OAI.CubicFirstMoment.stopped_core_cutoff line 11
  2. lemma OAI.CubicFirstMoment.stopped_large_core_scale line 20
  3. lemma OAI.CubicFirstMoment.stopped_length_log_power line 50