OAI/NumberTheory/TwoPoint/Halasz/HalaszMixedBounds.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Trivial estimates for the mixed prime convolution. The underlying prime values and the bounded typical cofactor are different sequences.

  1. def OAI.TwoPointCorrelations.halaszMixedGrouped line 14
  2. lemma OAI.TwoPointCorrelations.halasz_mixed_prime_term_bound line 19
  3. lemma OAI.TwoPointCorrelations.halasz_mixed_convolution_trivial line 37
  4. lemma OAI.TwoPointCorrelations.halasz_mixed_convolution_div_log line 55
  5. theorem OAI.TwoPointCorrelations.halasz_mixed_grouped_trivial line 91