OAI/NumberTheory/TwoPoint/Bounds/PrimeCostTails.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A fixed finite exclusion set makes all later finite prime costs small.

  1. lemma OAI.TwoPointCorrelations.summable_prime_cost_tail line 14
  2. lemma OAI.TwoPointCorrelations.pair_prime_defect_summable line 32
  3. lemma OAI.TwoPointCorrelations.exists_prime_defect_exclusion line 53