First moment: $\sum_{s\le x} r(s)\ge x^2/(9(\log x)^2)$

Proved

Schnir.first_moment

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

number-theoryschnirelmann-densitysieve-theory

Let $r(s)$ be the number of ordered pairs $(p,q)$ of odd primes with $p+q=s$ . For every real $x\ge 2000$ ,

\sum_{0\le s\le x} r(s) \;\ge\; \frac{x^2}{9(\log x)^2}.

This is the first-moment estimate with $c_1=1/9$ . Together with the second moment it shows, via Cauchy–Schwarz, that sums of two odd primes have positive density.

Formalization Note The sum runs over integers $0\le s\le\lfloor x\rfloor$ . $r$ is Schnir.r from Def_Schnir_defs.

Preamble

import Mathlib
import Definitions.Def_Schnir_defs

Formal statement

namespace Schnir

theorem first_moment (x : ℝ) (hx : 2000 ≤ x) :
    x ^ 2 / (9 * (Real.log x) ^ 2) ≤ ∑ s ∈ Finset.range (⌊x⌋₊ + 1), (r s : ℝ) := by sorry

end Schnir

Source

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

View graph

First moment: ∑s≤xr(s)≥x2/(9(log⁡x)2)\sum_{s\le x} r(s)\ge x^2/(9(\log x)^2)∑s≤x​r(s)≥x2/(9(logx)2)

First moment: $\sum_{s\le x} r(s)\ge x^2/(9(\log x)^2)$