OAI/NumberTheory/CubicMoment/Estimates/DivisorOuterMass.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Apply the outer cubic sieve to the literal shortened Poisson rows, uniformly in the two Mellin signs.

  1. theorem OAI.CubicFirstMoment.fullPrime_divisor_outer_mass line 13