ThetaToHarmonic.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Reciprocal-prime estimates derived from the published theta bound

theorem OAI.Ostmann.theta_to_harmonic_error line 15

Source documentation

The classical theta error on a multiplicative interval transfers with an absolute factor of eighteen, uniformly in the modulus and residue.

theorem theta_to_harmonic_error (q a : ℕ) (φ χ β c C : ℝ) (hβ : β ≠ 0)
    (hc : 0 ≤ c) (hC : 0 ≤ C) {u v : ℝ} (hu : 1 < u)
    (hlogu : 1 ≤ Real.log u) (huv : u ≤ v) (hshort : v ≤ 3 * u)
    (hθ : ∀ t ∈ Set.Icc u v,
      |primeProgressionTheta q a t - thetaMainTerm φ χ β t| ≤
        C * t * Real.exp (-c * Real.sqrt (Real.log t))) :
    |reciprocalPrimeInterval q a u v -
      ∫ t in Set.Ioc u v, primeHarmonicWeight t * thetaMainDensity φ χ β t| ≤
        18 * C * Real.exp (-c * Real.sqrt (Real.log u)) := by
…

Mentions: OAI.Ostmann.primeProgressionTheta, OAI.Ostmann.thetaMainTerm, OAI.Ostmann.reciprocalPrimeInterval, OAI.Ostmann.primeHarmonicWeight, OAI.Ostmann.thetaMainDensity

theorem OAI.Ostmann.exp_short_interval_le_three line 47
Source documentation
A log interval of length at most one is a multiplicative interval with ratio less than three, as required by the uniform partial-summation bound.
```
theorem exp_short_interval_le_three {s t : ℝ} (hst : t ≤ s + 1) :
    Real.exp t ≤ 3 * Real.exp s := by
…
```

theorem OAI.Ostmann.theta_to_log_interval_error line 57

Source documentation

The form used in the finite log-cell partition, before the harmless change of variables in the main integral.

theorem theta_to_log_interval_error (q a : ℕ) (φ χ β c C : ℝ) (hβ : β ≠ 0)
    (hc : 0 ≤ c) (hC : 0 ≤ C) {s t : ℝ} (hs : 1 ≤ s)
    (hst : s ≤ t) (hshort : t ≤ s + 1)
    (hθ : ∀ x ∈ Set.Icc (Real.exp s) (Real.exp t),
      |primeProgressionTheta q a x - thetaMainTerm φ χ β x| ≤
        C * x * Real.exp (-c * Real.sqrt (Real.log x))) :
    |reciprocalPrimeInterval q a (Real.exp s) (Real.exp t) -
      ∫ x in Set.Ioc (Real.exp s) (Real.exp t),
        primeHarmonicWeight x * thetaMainDensity φ χ β x| ≤
        18 * C * Real.exp (-c * Real.sqrt s) := by
…

Mentions: OAI.Ostmann.primeProgressionTheta, OAI.Ostmann.thetaMainTerm, OAI.Ostmann.reciprocalPrimeInterval, OAI.Ostmann.primeHarmonicWeight, OAI.Ostmann.thetaMainDensity