OAI/NumberTheory/CubicMoment/Estimates/PrimeModelLogTail.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The model is already negligible above a sufficiently large power of the logarithm. This leaves the genuinely low-height corrected sum.

  1. theorem OAI.CubicFirstMoment.prime_model_height_log_saving line 13
  2. theorem OAI.CubicFirstMoment.prime_model_cutoff_log_saving line 53
  3. theorem OAI.CubicFirstMoment.prime_model_log_window_sum_bound line 93
  4. lemma OAI.CubicFirstMoment.cubic_log_saving_isLittleO line 130
  5. theorem OAI.CubicFirstMoment.actual_prime_model_log_tail_isLittleO line 153