OAI/NumberTheory/CubicMoment/Estimates/ScaleFirstArity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Expand the rough remainder only after fixing the distinguished smooth scales. All tuple and product supports remain exact.

  1. def OAI.CubicFirstMoment.distinguishedScaleDoubleRow line 13
  2. theorem OAI.CubicFirstMoment.distinguishedScaleRow_remainder_arity line 22
  3. lemma OAI.CubicFirstMoment.distinguishedScaleDoubleRow_eq_tuples line 37
  4. lemma OAI.CubicFirstMoment.normTupleWeight_sum_elim line 99
  5. lemma OAI.CubicFirstMoment.distinguishedScaleDoubleRow_partition line 108