Prove2Me

Chebyshev-type lower bound π(y)−1≥2y/(3log⁡y)\pi(y)-1\ge 2y/(3\log y)

Proved
Schnir.pi_lower

by xuanji · Sep 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

number-theoryschnirelmann-densitysieve-theory

For every real y≥1000y\ge 1000,

π(y)−1  ≥  2y3log⁡y,\pi(y)-1 \;\ge\; \frac{2y}{3\log y},

where π(y)\pi(y) is the number of primes at most yy.

This elementary Chebyshev-type bound supplies all the prime-counting input of the argument: the first-moment lower bound for r(s)r(s) and the density of AA at moderate scales.

Formalization Note π(y)\pi(y) is Nat.primeCounting ⌊y⌋₊.

Preamble
import Mathlib
import Definitions.Def_Schnir_defs
Formal statement
namespace Schnir

theorem pi_lower (y : ℝ) (hy : 1000 ≤ y) :
    2 * y / (3 * Real.log y) ≤ (Nat.primeCounting ⌊y⌋₊ : ℝ) - 1 := by sorry

end Schnir
Source
An explicit elementary constant for sums of primes (unpublished note, September 2026), eq. (3), §1

View graph