ReciprocalPrimeBands.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Quantitative reciprocal-prime bands from the actual theta error. Partial summation gives the reciprocal-prime estimates.

def OAI.TwoPointCorrelations.reciprocalLog line 15
Also declared: OAI/NumberTheory/TwoPointCorrelations/ReciprocalPrimeBands.lean:15 (same declaration text).
lemma OAI.TwoPointCorrelations.reciprocalLog_hasDerivAt line 17
Also declared: OAI/NumberTheory/TwoPointCorrelations/ReciprocalPrimeBands.lean:17 (same declaration text).
lemma OAI.TwoPointCorrelations.reciprocalLog_error_le line 28
Also declared: OAI/NumberTheory/TwoPointCorrelations/ReciprocalPrimeBands.lean:28 (same declaration text).
lemma OAI.TwoPointCorrelations.reciprocalLog_deriv_error_le line 42
Also declared: OAI/NumberTheory/TwoPointCorrelations/ReciprocalPrimeBands.lean:42 (same declaration text).
theorem OAI.TwoPointCorrelations.reciprocal_band_error line 61
Source documentation
A uniform band error. The upper endpoint is arbitrary, so this applies simultaneously to all the logarithmically spaced supplies in the manuscript.
Also declared: OAI/NumberTheory/TwoPointCorrelations/ReciprocalPrimeBands.lean:61 (same declaration text).
```
theorem reciprocal_band_error (c : ℕ → ℝ) (α K a b : ℝ) (hK : 0 ≤ K)
    (ha : Real.exp 1 ≤ a) (hab : a ≤ b)
    (hE : ∀ x ∈ Set.Icc a b,
      |partialCoefficientSum c x - α * x| ≤ K * x / Real.log x ^ 2) :
    |(∑ n ∈ Ioc ⌊a⌋₊ ⌊b⌋₊, reciprocalLog n * c n) -
      α * (Real.log (Real.log b) - Real.log (Real.log a))| ≤ 4 * K / Real.log a := by
…
```
Mentions: OAI.TwoPointCorrelations.partialCoefficientSum, OAI.TwoPointCorrelations.reciprocalLog