Mean square of the arithmetic factor: $\sum_{s\le x,\,2\mid s} C(s)^2\le \tfrac{21}{2}x$

Proved

Schnir.C_mean

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

number-theoryschnirelmann-densitysieve-theory

For every real $x\ge 0$ ,

\sum_{\substack{1\le s\le x\\ s \text{ even}}} C(s)^2 \;\le\; \frac{21}{2}\,x, \qquad C(s)=\prod_{p\mid s}\left(1+\frac{p}{(p-1)^2}\right).

This controls the average size of the arithmetic factor in the pointwise sieve bound, which is what the second moment needs.

Formalization Note The sum is over even integers $1\le s\le\lfloor x\rfloor$ .

Preamble

import Mathlib
import Definitions.Def_Schnir_defs

Formal statement

namespace Schnir

theorem C_mean (x : ℝ) (hx : 0 ≤ x) :
    ∑ s ∈ (Finset.Icc 1 ⌊x⌋₊).filter Even, (C s) ^ 2 ≤ 21 / 2 * x := by sorry

end Schnir

Source

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

Mean square of the arithmetic factor: ∑s≤x, 2∣sC(s)2≤212x\sum_{s\le x,\,2\mid s} C(s)^2\le \tfrac{21}{2}x∑s≤x,2∣s​C(s)2≤221​x