OAI/NumberTheory/TwoPoint/Bounds/MultiplicativePrimeProducts.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Finite squarefree products of an ordinary multiplicative function, and the elementary defect inequality used in selecting raw divisors.

  1. lemma OAI.TwoPointCorrelations.Multiplicative.prime_product line 14
  2. lemma OAI.TwoPointCorrelations.one_sub_prod_le_sum line 31
  3. lemma OAI.TwoPointCorrelations.multiplicative_prime_product_defect line 47
  4. lemma OAI.TwoPointCorrelations.prime_product_pair_defect line 64