OAI/NumberTheory/TwoPoint/Halasz/HalaszMixedInner.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The inner logarithmic approximation for the actual typical sequence. The same estimate covers cofactors shorter than the deleted-prime cutoff.

  1. lemma OAI.TwoPointCorrelations.halasz_mixed_logarithmic_approximation_all line 13
  2. lemma OAI.TwoPointCorrelations.halasz_mixed_prefix_log line 45
  3. lemma OAI.TwoPointCorrelations.halasz_mixed_real_log_approximation line 61
  4. lemma OAI.TwoPointCorrelations.halasz_mixed_real_inner_approximation line 99