OAI/NumberTheory/TwoPoint/Walks/RetainedRowScale.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

At a fixed W the retained row majorant grows polynomially in L; it can therefore be absorbed into a small exponential boundary budget.

  1. lemma OAI.TwoPointCorrelations.primeSupplyCount_le_log line 13
  2. lemma OAI.TwoPointCorrelations.retained_row_exponential_bound line 19
  3. lemma OAI.TwoPointCorrelations.eventually_retained_row_scale line 50
  4. lemma OAI.TwoPointCorrelations.eventually_const_le_exp_quarter line 67