OAI/NumberTheory/TwoPoint/Halasz/HalaszMixedConvolution.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Logarithmic convolution for a typical coefficient. Only multiplication by primes above the deleted bands is used. The prime coefficient and the remaining typical coefficient are kept distinct.

  1. def OAI.TwoPointCorrelations.halaszRawPrimeTerm line 14
  2. def OAI.TwoPointCorrelations.halaszMixedPrimeConvolution line 17
  3. lemma OAI.TwoPointCorrelations.halasz_raw_logarithmic_sum line 21
  4. lemma OAI.TwoPointCorrelations.halasz_raw_row_bound line 51
  5. lemma OAI.TwoPointCorrelations.halasz_raw_prime_term_bound line 64
  6. lemma OAI.TwoPointCorrelations.halasz_raw_prime_power_error line 75
  7. lemma OAI.TwoPointCorrelations.halasz_raw_prime_band_error line 107
  8. theorem OAI.TwoPointCorrelations.halasz_mixed_logarithmic_approximation line 125