HalaszInnerApproximation.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

A complex-valued approximation, not just a norm bound, permits a second application of the prime convolution inside the first one.

lemma OAI.TwoPointCorrelations.halasz_prime_log_approximation line 12
Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszInnerApproximation.lean:12 (same declaration text).
lemma OAI.TwoPointCorrelations.halasz_prime_inner_approximation line 27
Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszInnerApproximation.lean:27 (same declaration text).
def OAI.TwoPointCorrelations.halaszInnerErrorConstant line 43
Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszInnerApproximation.lean:43 (same declaration text).
lemma OAI.TwoPointCorrelations.halaszInnerErrorConstant_nonneg line 46
Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszInnerApproximation.lean:46 (same declaration text).
lemma OAI.TwoPointCorrelations.halasz_real_log_approximation line 54
Source documentation
The logarithm may use the real cutoff, while the sum and convolution retain the exact natural cutoff. Their rounding error is uniformly O(x).
Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszInnerApproximation.lean:54 (same declaration text).
```
lemma halasz_real_log_approximation (f : ℕ → ℂ) (hf : OneBounded f)
    (hmul : ∀ m n : ℕ, 0 < m → 0 < n → f (m * n) = f m * f n)
    (M : ℕ) (hM : 1 ≤ M) {x : ℝ} (hMx : (M : ℝ) ≤ x) (hxM : x ≤ 2 * M) :
    ‖(∑ n ∈ Icc 1 M, f n) * (Real.log x : ℂ) -
      halaszPrimeConvolution f M‖ ≤ halaszInnerErrorConstant * x := by
…
```
Mentions: OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.halaszPrimeConvolution, OAI.TwoPointCorrelations.halaszInnerErrorConstant
lemma OAI.TwoPointCorrelations.halasz_real_inner_approximation line 84
Also declared: OAI/NumberTheory/TwoPoint/Halasz/HalaszInnerApproximation.lean:84 (same declaration text).