Quantitative logarithmic gain from saved prime factors #
The error in a lower bound for the rough logarithmic mass must be smaller
than the saving from divisor hits. A merely qualitative o(1) relative
error does not supply the quantitative conclusion used in Theorem 2.
theorem
NairTenenbaum.exp_gain_of_logMass_bounds
{P y a H E M : ℝ}
(hP : 1 ≤ P)
(hy : 1 ≤ y)
(ha : 0 < a)
(hH : 0 ≤ H)
(hHa : H ≤ a)
(hlower : a * Real.log y - E ≤ M)
(hupper : M ≤ (a - H) * Real.log P)
(herror : E ≤ H * Real.log y / 2)
:
Convert logarithmic mass and a factor-count saving into an exponential
lower bound. E is the absolute error in the mass estimate.