OAI/NumberTheory/CubicMoment/Estimates/LongPrimeParameterScale.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Fixed powers of log X fit the prime parameter log X/4 after a one-unit exponent enlargement. This is uniform in all arithmetic data.

  1. theorem OAI.CubicFirstMoment.eventually_log_parameter_power line 11
  2. lemma OAI.CubicFirstMoment.prime_parameter_log_saving line 30