OAI/NumberTheory/CubicMoment/Decomposition/DistinguishedScaleRows.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Exact scale-first decomposition of the central rough product. The threshold applies to independent distinguished-prime scales, before expanding the rough remainder.

  1. def OAI.CubicFirstMoment.distinguishedScaleRow line 14
  2. def OAI.CubicFirstMoment.distinguishedLowScaleRows line 22
  3. def OAI.CubicFirstMoment.distinguishedHighScaleRows line 27
  4. lemma OAI.CubicFirstMoment.distinguishedScaleRows_split line 32
  5. lemma OAI.CubicFirstMoment.distinguishedScaleRows_eq_arity line 44
  6. theorem OAI.CubicFirstMoment.centralRoughProduct_by_distinguished_scale line 60
  7. lemma OAI.CubicFirstMoment.distinguishedScaleRow_low_restrict line 96