OAI/NumberTheory/CubicMoment/Decomposition/StoppedDivisorScale.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Elementary scaling of the unrestricted sieve on shortened rows.

  1. lemma OAI.CubicFirstMoment.quotient_power_times_self line 9
  2. lemma OAI.CubicFirstMoment.stopped_outer_row_scale line 16
  3. lemma OAI.CubicFirstMoment.stopped_outer_row_scale_le line 35