OAI/NumberTheory/CubicMoment/Estimates/PrimeGroupTailSieve.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

An actual finite frequency-block estimate for arbitrary squarefree coefficients. There is no prime-convolution or height restriction.

  1. theorem OAI.CubicFirstMoment.primeGroupTail_frequency_sieve line 11