OAI/NumberTheory/CubicMoment/Estimates/PrimeCommonRows.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Arithmetic bounds for the actual common-factor quotient rows.

  1. lemma OAI.CubicFirstMoment.fullPrime_residual_norms line 14
  2. lemma OAI.CubicFirstMoment.fullPrime_nonunit_common_factor_large line 27
  3. lemma OAI.CubicFirstMoment.fullPrime_common_energy_bound line 52