OAI/NumberTheory/TwoPoint/Walks/SelectedPairCosts.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Passing the proved prime-cost moments to arbitrary selected pair subfamilies.

  1. lemma OAI.TwoPointCorrelations.selected_pair_mass_le line 12
  2. lemma OAI.TwoPointCorrelations.selected_pair_prime_cost_le line 19
  3. lemma OAI.TwoPointCorrelations.selected_pair_reciprocal_cost_le line 40