OAI/NumberTheory/CubicMoment/Estimates/LargeDivisorLogSaving.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Large common prime divisors have an arbitrary logarithmic saving for the actual full prime-convolution mass. The bound follows from the outer sieve, shortened energy sum, and elementary power gap.

  1. theorem OAI.CubicFirstMoment.fullPrime_large_divisor_log_saving line 18