HalaszUnitMean.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

An ordinary absolute mean bound for the constant-one correction. A positive logarithmic convolution and the finite Euler bound retain the full prime-discrepancy exponent.

lemma OAI.TwoPointCorrelations.halasz_real_hyperbola line 15
Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszUnitMean.lean:15 (same declaration text).
lemma OAI.TwoPointCorrelations.halasz_unit_logarithmic_sum line 22
Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszUnitMean.lean:22 (same declaration text).
lemma OAI.TwoPointCorrelations.halasz_positive_log_to_mean line 59
Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszUnitMean.lean:59 (same declaration text).
theorem OAI.TwoPointCorrelations.halasz_unit_correction_mean line 76
Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszUnitMean.lean:76 (same declaration text).
theorem OAI.TwoPointCorrelations.halasz_near_correction_mean line 102
Source documentation
Near the minimizing twist the absolute unit correction has a genuine logarithmic saving, uniformly over all allowed missing-band masks.
Also declared: OAI/NumberTheory/TwoPointCorrelations/HalaszUnitMean.lean:102 (same declaration text).
```
theorem halasz_near_correction_mean :
    ∀ᶠ N : ℕ in Filter.atTop, ∀ (F : ℕ → ℂ), F 1 = 1 → OneBounded F →
      ∀ (Q : Finset ℕ), (∀ p ∈ Q, p.Prime) →
      (∀ p ∈ Q, (p : ℝ) ≤ Real.exp (Real.sqrt (Real.log N))) →
      ∀ t : ℝ, squaredDistance F (mrtArchimedeanTwist t) N ≤
        Real.log (Real.log N) / 8 →
      (∑ n ∈ Icc 1 N,
        ‖halaszUnitCorrection (halaszTwistedFunction (mrtMissingCoefficient F Q) t) n‖) ≤
          ((halaszPrimePowerLogConstant + 1) * Real.exp 8) * N *
            (Real.log N) ^ (-1 / (8 : ℝ)) := by
…
```
Mentions: OAI.TwoPointCorrelations.OneBounded, OAI.TwoPointCorrelations.mrtArchimedeanTwist, OAI.TwoPointCorrelations.halaszUnitCorrection, OAI.TwoPointCorrelations.halaszTwistedFunction, OAI.TwoPointCorrelations.mrtMissingCoefficient, OAI.TwoPointCorrelations.halaszPrimePowerLogConstant