OAI/NumberTheory/CubicMoment/Estimates/CommonRemainderBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Bound the noncoprime remainder by the energy of the genuine common-factor blocks, and then by the original prime-convolution energy.

  1. theorem OAI.CubicFirstMoment.primaryMass_sub_coprime_outer line 12
  2. theorem OAI.CubicFirstMoment.fullPrime_divisor_noncoprime_outer line 49