PrimeLogDensity.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The retained Page density in logarithmic coordinates

def OAI.Ostmann.primeLogDensity line 11
theorem OAI.Ostmann.thetaMain_log_substitution line 16
Source documentation
The Jacobian cancels the 1/x part of the harmonic weight. The exceptional contribution has no extra factor of its zero β.
```
theorem thetaMain_log_substitution (φ χ β : ℝ) {s t : ℝ}
    (hs : 0 < s) (hst : s ≤ t) :
    (∫ x in Set.Ioc (Real.exp s) (Real.exp t),
      primeHarmonicWeight x * thetaMainDensity φ χ β x) =
        ∫ y in Set.Ioc s t, primeLogDensity φ χ β y := by
…
```
Mentions: OAI.Ostmann.primeHarmonicWeight, OAI.Ostmann.thetaMainDensity, OAI.Ostmann.primeLogDensity

theorem OAI.Ostmann.prime_log_interval_error line 50

Source documentation

The actual reciprocal-prime interval estimate in logarithmic coordinates, proved from the precise theta estimate.

theorem prime_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) -
      ∫ y in Set.Ioc s t, primeLogDensity φ χ β y| ≤
        18 * C * Real.exp (-c * Real.sqrt s) := by
…

Mentions: OAI.Ostmann.primeProgressionTheta, OAI.Ostmann.thetaMainTerm, OAI.Ostmann.reciprocalPrimeInterval, OAI.Ostmann.primeLogDensity