OAI/NumberTheory/CubicMoment/Estimates/CommonGramRemainder.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Separate the coprime term from the exact common-factor expansion. Only nonunit common factors remain, so roughness shortens every row.

  1. def OAI.CubicFirstMoment.commonGramBlock line 12
  2. lemma OAI.CubicFirstMoment.commonGramBlock_moebius line 17
  3. theorem OAI.CubicFirstMoment.primaryMass_sub_coprime_common line 53
  4. lemma OAI.CubicFirstMoment.divisorCoprimeDispersionGram_eq_coprimeGram line 98
  5. theorem OAI.CubicFirstMoment.divisorVariance_sub_coprime_common line 114