OAI/NumberTheory/TwoPoint/Walks/TuplePrimeCosts.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

First moments of additive prime costs for the actual disjoint-band tuple family. Large band masses dilute any fixed summable prime defect.

  1. lemma OAI.TwoPointCorrelations.tuple_coordinate_cost_sum line 13
  2. lemma OAI.TwoPointCorrelations.primeTupleDivisors_cost_sum line 49
  3. lemma OAI.TwoPointCorrelations.primeTupleDivisors_cost_bound line 73