PrimeHarmonicWeightBounds.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Explicit variation cost on a short logarithmic interval

theorem OAI.Ostmann.primeHarmonicWeight_le line 11
theorem OAI.Ostmann.primeHarmonicDerivative_le line 20

theorem OAI.Ostmann.primeHarmonic_short_interval_error line 43

Source documentation

A theta error of size E on an interval with v ≤ 3u costs at most 6E/u in the reciprocal-prime measure.

theorem primeHarmonic_short_interval_error (q a : ℕ) (φ χ β : ℝ) (hβ : β ≠ 0)
    {u v : ℝ} (hu : 1 < u) (hlogu : 1 ≤ Real.log u)
    (huv : u ≤ v) (hshort : v ≤ 3 * u) (E : ℝ) (hE : 0 ≤ E)
    (hθ : ∀ t ∈ Set.Icc u v, |primeProgressionTheta q a t - thetaMainTerm φ χ β t| ≤ E) :
    |reciprocalPrimeInterval q a u v -
      ∫ t in Set.Ioc u v, primeHarmonicWeight t * thetaMainDensity φ χ β t| ≤ 6 * E / u := by
…

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