Prove2Me

Pointwise bound r(s)≤9C(s) s/(log⁡s)2r(s)\le 9C(s)\,s/(\log s)^2

Proved
Schnir.pointwise_bound

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

number-theoryschnirelmann-densitysieve-theory

For every even integer s≥e1000s\ge e^{1000},

r(s)  ≤  9 C(s) s(log⁡s)2,r(s) \;\le\; 9\,C(s)\,\frac{s}{(\log s)^2},

where r(s)r(s) counts ordered pairs of odd primes summing to ss and C(s)=∏p∣s(1+p(p−1)2)C(s)=\prod_{p\mid s}\left(1+\frac{p}{(p-1)^2}\right).

This is the explicit upper-bound-sieve estimate for Goldbach representations, obtained with sieve level z=s/(log⁡s)2z=\sqrt{s}/(\log s)^2.

Formalization Note rr and CC are Schnir.r and Schnir.C.

Preamble
import Mathlib
import Definitions.Def_Schnir_defs
Formal statement
namespace Schnir

theorem pointwise_bound (s : ℕ) (hs : Even s) (hbig : Real.exp 1000 ≤ s) :
    (r s : ℝ) ≤ 9 * C s * s / (Real.log s) ^ 2 := by sorry

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

View graph