OAI/NumberTheory/CubicMoment/Estimates/SievedSquarefreeModel.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual positive square-divisor variance has the true squarefree model mass. This is the positive term of the corrected-square argument.

  1. theorem OAI.CubicFirstMoment.sieved_squarefree_model_asymptotic line 13