PrimeLogDensityBounds.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Bounds on the retained density and on discarded real zeros

theorem OAI.Ostmann.continuousOn_primeLogDensity line 12
theorem OAI.Ostmann.primeLogDensity_bounds line 25

theorem OAI.Ostmann.primeLogDensity_correction_le line 35

Source documentation

A zero separated from one by d contributes at most exp (-d*s) throughout a logarithmic interval beginning at s ≥ 1.

theorem primeLogDensity_correction_le (φ χ β d : ℝ) (hφ : 1 ≤ φ)
    (hχ : |χ| ≤ 1) (hd : 0 ≤ d) (hβ : β ≤ 1 - d)
    {s y : ℝ} (hs : 1 ≤ s) (hsy : s ≤ y) :
    |primeLogDensity φ χ β y - primeLogDensity φ 0 1 y| ≤
      Real.exp (-d * s) := by
…

Mentions: OAI.Ostmann.primeLogDensity

theorem OAI.Ostmann.primeLogDensity_integral_correction_le line 58