OAI/NumberTheory/TwoPoint/Halasz/HalaszPrimeMass.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Mertens' first theorem, in the prime-band convention needed for the small- and large-prime truncations in the Halasz convolution.

  1. def OAI.TwoPointCorrelations.halaszMertensConstant line 13

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

  2. lemma OAI.TwoPointCorrelations.halaszMertensConstant_nonneg line 15

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszPrimeMass.lean:15 (same declaration text).

  3. lemma OAI.TwoPointCorrelations.halasz_prime_prefix_mass line 19

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

  4. lemma OAI.TwoPointCorrelations.halasz_prime_band_mass line 25

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszPrimeMass.lean:25 (same declaration text).

  5. lemma OAI.TwoPointCorrelations.halasz_prime_band_mertens line 32

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszPrimeMass.lean:32 (same declaration text).

  6. lemma OAI.TwoPointCorrelations.halasz_prime_prefix_mass_le line 45

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszPrimeMass.lean:45 (same declaration text).

  7. lemma OAI.TwoPointCorrelations.halasz_prime_band_mass_le line 50

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszPrimeMass.lean:50 (same declaration text).

  8. lemma OAI.TwoPointCorrelations.halasz_upper_half_prime_mass line 55

    Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszPrimeMass.lean:55 (same declaration text).