Selberg upper-bound sieve with explicit error term

Proved

Schnir.sieve_ineq

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. Let $S_s(z)$ count the integers $1\le a\le s$ such that $a(s-a)$ has no prime divisor at most $z$ , and let $G_s(z)=\sum_{d\le z,\,d\text{ squarefree}} h_s(d)$ with $h_s(d)=\prod_{p\mid d}\rho_s(p)/(p-\rho_s(p))$ , where $\rho_s(p)=1$ if $p\mid s$ and $\rho_s(p)=2$ otherwise. Then

S_s(z) \;\le\; \frac{s}{G_s(z)} + z^2(1+\log z)^2 .

This is Selberg's $\Lambda^2$ upper-bound sieve for the pairs $\{a, s-a\}$ , with a fully explicit error term. It is the main analytic input of the argument.

Formalization Note $S_s$ , $G_s$ and $h_s$ are Schnir.S, Schnir.G and Schnir.hfun from Def_Schnir_defs.

Preamble

import Mathlib
import Definitions.Def_Schnir_defs

Formal statement

namespace Schnir

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

end Schnir

Source

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

View graph