PrimeIntervalVariation.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Weighted short prime intervals from the published progression input

theorem OAI.Ostmann.reciprocalPrimeInterval_add line 13
theorem OAI.Ostmann.primeLogDensity_integral_add line 18
def OAI.Ostmann.selectedPrimeLogDensity line 30
Source documentation
The reference density is the actual selected Page-corrected density. It stays inside the integral throughout weighted summation.
```
noncomputable def selectedPrimeLogDensity (P : PublishedProgressionInput) (Q q a : ℕ) : ℝ → ℝ :=
…
```
Mentions: OAI.Ostmann.PublishedProgressionInput

theorem OAI.Ostmann.PublishedProgressionInput.weighted_prime_interval_variation line 38

Source documentation

Finite Abel summation turns the uniform interval error into a variation error for the actual complex weights. There is no factor for the number of partition intervals.

theorem PublishedProgressionInput.weighted_prime_interval_variation
    (P : PublishedProgressionInput) {Q q a : ℕ}
    (hQ : 2 ≤ Q) (hq : 1 ≤ q) (hqQ : q ≤ Q) (ha : a.Coprime q)
    (s : ℕ → ℝ) (hs : Monotone s) (hs0 : 1 ≤ s 0) (N : ℕ) (hshort : s N ≤ s 0 + 1)
    (w : ℕ → ℂ) :
    ‖∑ j ∈ Finset.range N, w j *
      ((reciprocalPrimeInterval q a (Real.exp (s j)) (Real.exp (s (j + 1))) -
        ∫ y in Set.Ioc (s j) (s (j + 1)), selectedPrimeLogDensity P Q q a y : ℝ) : ℂ)‖ ≤
      discreteVariation w N *
        (18 * P.errorConstant * Real.exp (-P.decay * Real.sqrt (s 0)) +
          Real.exp (-P.kappa * s 0 / Real.log (4 * (Q : ℝ)))) := by
…

Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.reciprocalPrimeInterval, OAI.Ostmann.selectedPrimeLogDensity, OAI.Ostmann.discreteVariation