OAI/NumberTheory/CubicMoment/Estimates/CommonVarianceDecomposition.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The square-divisor variance as actual character mass, followed by its canonical common-factor decomposition. This is the bridge to the wide dual recurrence on shortened rows.

  1. def OAI.CubicFirstMoment.divisorGramCoefficient line 14
  2. lemma OAI.CubicFirstMoment.divisorGramCoefficient_norm_le line 17
  3. lemma OAI.CubicFirstMoment.divisorDispersionVariance_eq_primaryMass line 27
  4. theorem OAI.CubicFirstMoment.divisorDispersionVariance_common_grams line 45