HalaszPrimeConvolution.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Prime-only convolution and its explicit O(N) error. This is the first step of the Granville--Harper--Soundararajan double-convolution argument.

def OAI.TwoPointCorrelations.halaszPrimeConvolution line 14
Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszPrimeConvolution.lean:14 (same declaration text).
lemma OAI.TwoPointCorrelations.halasz_log_sum_rows line 18
Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszPrimeConvolution.lean:18 (same declaration text).
lemma OAI.TwoPointCorrelations.halasz_prime_convolution_difference line 29
Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszPrimeConvolution.lean:29 (same declaration text).
theorem OAI.TwoPointCorrelations.halasz_log_sum_prime_error line 43
Source documentation
The exact logarithmic sum differs from its prime-only convolution by at most a constant times N, uniformly in the bounded multiplicative function.
Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszPrimeConvolution.lean:43 (same declaration text).
```
theorem halasz_log_sum_prime_error (f : ℕ → ℂ) (hbound : OneBounded f)
    (hmul : ∀ m n : ℕ, 0 < m → 0 < n → f (m * n) = f m * f n) (N : ℕ) :
    ‖(∑ n ∈ Icc 1 N, f n * (Real.log (n : ℝ) : ℂ)) - halaszPrimeConvolution f N‖ ≤
      (N : ℝ) * halaszPrimePowerConstant := by
…
```
Mentions: OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.halaszPrimeConvolution, OAI.TwoPointCorrelations.halaszPrimePowerConstant
theorem OAI.TwoPointCorrelations.halasz_prime_convolution_mean_bound line 51
Source documentation
First Halasz reduction, with a uniform and completely proved error.
Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszPrimeConvolution.lean:51 (same declaration text).
```
theorem halasz_prime_convolution_mean_bound (f : ℕ → ℂ) (hbound : OneBounded f)
    (hmul : ∀ m n : ℕ, 0 < m → 0 < n → f (m * n) = f m * f n)
    (N : ℕ) (hN : 1 ≤ N) :
    Real.log (N : ℝ) * ‖∑ n ∈ Icc 1 N, f n‖ ≤
      ‖halaszPrimeConvolution f N‖ + (halaszPrimePowerConstant + 1) * (N : ℝ) := by
…
```
Mentions: OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.halaszPrimeConvolution, OAI.TwoPointCorrelations.halaszPrimePowerConstant