Second moment: $\sum_{s\le x} r(s)^2\le 860\,x^3/(\log x)^4$

Proved

Schnir.second_moment

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

number-theoryschnirelmann-densitysieve-theory

For every real $x\ge e^{2000}$ ,

\sum_{0\le s\le x} r(s)^2 \;\le\; 860\,\frac{x^3}{(\log x)^4}.

This is the second-moment estimate with $c_2=860$ and $x_0=e^{2000}$ .

Formalization Note The sum runs over integers $0\le s\le\lfloor x\rfloor$ .

Preamble

import Mathlib
import Definitions.Def_Schnir_defs

Formal statement

namespace Schnir

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

end Schnir

Source

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

View graph

Second moment: ∑s≤xr(s)2≤860 x3/(log⁡x)4\sum_{s\le x} r(s)^2\le 860\,x^3/(\log x)^4∑s≤x​r(s)2≤860x3/(logx)4

Second moment: $\sum_{s\le x} r(s)^2\le 860\,x^3/(\log x)^4$