OAI/NumberTheory/CubicMoment/Decomposition/StoppedPrimeScale.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The actual complementary norm and exclusion bounds needed to put stopped prime rows on the parameter log X/4.

  1. lemma OAI.CubicFirstMoment.stopped_complement_power_bound line 12
  2. lemma OAI.CubicFirstMoment.stopped_complement_exclusion_log line 21
  3. lemma OAI.CubicFirstMoment.geometricBinCount_logarithmic_width line 37