OAI/NumberTheory/TwoPoint/Bounds/PairPrimeCosts.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The tensor product of the tuple and padding laws retains separate first moments, rather than the largest prime cost of an individual divisor.

  1. lemma OAI.TwoPointCorrelations.pair_prime_cost_sum line 14
  2. lemma OAI.TwoPointCorrelations.tuple_padding_coprime line 55
  3. lemma OAI.TwoPointCorrelations.tuple_padding_prime_cost_bound line 71