OAI/NumberTheory/TwoPoint/Halasz/HalaszLogBands.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Mertens weights on the geometric bands of log(X/p) in the adaptive double convolution. The bounds remain valid for the last band near p=2.

  1. lemma OAI.TwoPointCorrelations.halasz_mem_prime_band line 13

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszLogBands.lean:13 (same declaration text).

  2. lemma OAI.TwoPointCorrelations.halasz_log_band_endpoints line 23

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszLogBands.lean:23 (same declaration text).

  3. theorem OAI.TwoPointCorrelations.halasz_log_band_mass line 39

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszLogBands.lean:39 (same declaration text).

  4. theorem OAI.TwoPointCorrelations.halasz_log_band_mass_linear line 80

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszLogBands.lean:80 (same declaration text).