OAI/NumberTheory/TwoPointCorrelations/HalaszPrimePolynomial.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The finite prime factors in the Perron integrand, with the same normalization as the prime mean-square theorem.

  1. def OAI.TwoPointCorrelations.halaszPrimePolynomial line 14

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszPrimePolynomial.lean:14 (same declaration text).

  2. lemma OAI.TwoPointCorrelations.halasz_prime_polynomial_series line 18

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszPrimePolynomial.lean:18 (same declaration text).

  3. lemma OAI.TwoPointCorrelations.halasz_prime_polynomial_continuous line 29

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszPrimePolynomial.lean:29 (same declaration text).

  4. lemma OAI.TwoPointCorrelations.halasz_prime_polynomial_norm line 32

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszPrimePolynomial.lean:32 (same declaration text).

  5. lemma OAI.TwoPointCorrelations.halasz_prime_polynomial_bounded line 41

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszPrimePolynomial.lean:41 (same declaration text).

  6. lemma OAI.TwoPointCorrelations.halasz_prime_coefficient_square_mass line 51

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszPrimePolynomial.lean:51 (same declaration text).

  7. lemma OAI.TwoPointCorrelations.halasz_adaptive_coefficient_bound line 61

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszPrimePolynomial.lean:61 (same declaration text).

  8. lemma OAI.TwoPointCorrelations.halasz_finite_prime_mangoldt_bound line 69

    Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszPrimePolynomial.lean:69 (same declaration text).