OAI/NumberTheory/CubicMoment/Estimates/PrimeTailCoefficientEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform second moments of the finite squarefree prime convolutions with unit coordinate weights. Only actual support counting and finite multiplicity are used.

  1. lemma OAI.CubicFirstMoment.fullPrimeCoefficient_l2_unit line 13