Lower bound $G_s(z)\ge (\log z)^2/(2C(s))$ for the sieve denominator

Proved

Schnir.G_lower

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

number-theoryschnirelmann-densitysieve-theory

Let $s$ be a positive even integer and $z>1$ real. With $G_s(z)$ the Selberg sieve denominator and $C(s)=\prod_{p\mid s}\left(1+\frac{p}{(p-1)^2}\right)$ ,

G_s(z) \;\ge\; \frac{(\log z)^2}{2\,C(s)} .

Combined with the sieve inequality, this bounds the sifted count by $2C(s)\,s/(\log z)^2$ plus the error term.

Formalization Note $G$ and $C$ are Schnir.G and Schnir.C from Def_Schnir_defs.

Preamble

import Mathlib
import Definitions.Def_Schnir_defs

Formal statement

namespace Schnir

theorem G_lower (s : ℕ) (hs : Even s) (hs0 : 0 < s) (z : ℝ) (hz : 1 < z) :
    (Real.log z) ^ 2 / (2 * C s) ≤ G s z := by sorry

end Schnir

Source

An explicit elementary constant for sums of primes (unpublished note, September 2026), eq. (10), §2.2

View graph

Lower bound Gs(z)≥(log⁡z)2/(2C(s))G_s(z)\ge (\log z)^2/(2C(s))Gs​(z)≥(logz)2/(2C(s)) for the sieve denominator

Lower bound $G_s(z)\ge (\log z)^2/(2C(s))$ for the sieve denominator