OAI/NumberTheory/CubicMoment/Decomposition/DistinguishedScalePartition.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The manuscript partitions the distinguished prime scales before splitting the rough remainder. This exact finite partition introduces no partial-product cutoff in a high-scale coefficient.

  1. def OAI.CubicFirstMoment.distinguishedScaleLength line 15
  2. def OAI.CubicFirstMoment.distinguishedScaleCoefficient line 18
  3. lemma OAI.CubicFirstMoment.distinguishedScaleCoefficient_partition line 26
  4. lemma OAI.CubicFirstMoment.distinguishedScaleCoefficient_range line 56
  5. lemma OAI.CubicFirstMoment.distinguishedScaleCoefficient_norm line 88
  6. lemma OAI.CubicFirstMoment.eventually_distinguishedScale_low_initial line 97