OAI/NumberTheory/TwoPoint/Bounds/SmoothProductBounds.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Elementary bounds for the Euler cost of adjoining retained tuple primes.

  1. lemma OAI.TwoPointCorrelations.one_le_smoothReciprocalProduct line 12
  2. lemma OAI.TwoPointCorrelations.smoothReciprocalProduct_union_le line 23
  3. lemma OAI.TwoPointCorrelations.smoothReciprocalProduct_mul_le line 37
  4. lemma OAI.TwoPointCorrelations.reciprocal_one_sub_le_exp line 45
  5. lemma OAI.TwoPointCorrelations.smooth_half_product_exp_bound line 54
  6. lemma OAI.TwoPointCorrelations.smooth_half_product_le_two line 69