OAI/NumberTheory/TwoPoint/Bounds/PrimeRowMomentScale.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The rare-site row majorant has a fixed polynomial second moment, uniformly in the band-width parameter W.

  1. lemma OAI.TwoPointCorrelations.prime_row_moment_product_bound line 13
  2. lemma OAI.TwoPointCorrelations.FiniteLaw.square_event_average_le line 75
  3. theorem OAI.TwoPointCorrelations.ProhibitedPrimeFamily.prime_row_second_moment_polynomial line 94
  4. theorem OAI.TwoPointCorrelations.ProhibitedPrimeFamily.prime_row_rare_square_bound line 107