Documentation

LeanPool.NairTenenbaum.Results.TheoremTwo

Theorem 2: a large prime factor in a short polynomial-value product #

The sharp small-prime logarithmic estimate leaves a linear error in the rough mass. The unconditional divisor-hit estimate absorbs that error and supplies the logarithmic exponential gain, with the strict exponent margin in the paper.