OAI/NumberTheory/CubicMoment/Estimates/LongPrimePowers.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Polynomial losses in log X are negligible on the actual long-prime scale exp(sqrt(log X)). This includes logarithmic prime exclusions.

  1. theorem OAI.CubicFirstMoment.long_prime_power_absorption line 11