OAI/NumberTheory/CubicMoment/Decomposition/StoppedProductMean.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Ordinary means for the squarefree product model of stopped coefficients. The product and norm multiplicities are both retained in an explicit fixed divisor moment, which costs a logarithm rather than a power of the length.

  1. lemma OAI.CubicFirstMoment.divisor_model_coefficient_energy line 16
  2. theorem OAI.CubicFirstMoment.divisor_model_height_mean line 44