OAI/NumberTheory/TwoPoint/Halasz/HalaszPrimePowerLogBound.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A Chebyshev bound for the prime-power logarithmic kernel appearing in the positive correction mean. Higher prime powers cost only an absolute constant times the cutoff.

  1. def OAI.TwoPointCorrelations.halaszPrimePowerLogConstant line 16

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszPrimePowerLogBound.lean:16 (same declaration text).

  2. lemma OAI.TwoPointCorrelations.halasz_log_sq_sqrt line 19

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszPrimePowerLogBound.lean:19 (same declaration text).

  3. lemma OAI.TwoPointCorrelations.halasz_prime_power_log_term line 27

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszPrimePowerLogBound.lean:27 (same declaration text).

  4. lemma OAI.TwoPointCorrelations.halasz_prime_power_log_sum line 48

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszPrimePowerLogBound.lean:48 (same declaration text).