OAI/NumberTheory/CubicMoment/Estimates/FullPrimeRoughDivisor.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A nontrivial common prime divisor of a rough prime convolution is itself large. In the retained small-divisor range only the empty subset survives; its coefficient remains the original convolution.

  1. lemma OAI.CubicFirstMoment.fullPrime_prime_divisor_coordinate line 15
  2. lemma OAI.CubicFirstMoment.fullPrime_nonempty_divisor_large line 27
  3. lemma OAI.CubicFirstMoment.fullPrime_small_divisor_slice_empty line 44