OAI/NumberTheory/TwoPoint/Halasz/HalaszMixedDouble.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Two logarithmic convolutions with a prime cutoff above every selected typical band. No multiplicativity of the typical coefficient is asserted.

  1. def OAI.TwoPointCorrelations.halaszMixedDouble line 15
  2. def OAI.TwoPointCorrelations.halaszMixedErrorConstant line 18
  3. lemma OAI.TwoPointCorrelations.halasz_mixed_error_nonneg line 21
  4. theorem OAI.TwoPointCorrelations.halasz_mixed_double_error line 29
  5. lemma OAI.TwoPointCorrelations.halasz_mixed_upper_truncation line 59
  6. theorem OAI.TwoPointCorrelations.halasz_mixed_double_mean line 82