Prove2Me

Schnirelmann's inequality σ(D+E)≥σ(D)+σ(E)−σ(D)σ(E)\sigma(D+E)\ge\sigma(D)+\sigma(E)-\sigma(D)\sigma(E)

Proved
Schnir.schnirelmann_ineq

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

number-theoryschnirelmann-densitysieve-theory

Let D,E⊆Z≥0D,E\subseteq\mathbb{Z}_{\ge 0} with 0∈D0\in D and 0∈E0\in E, and let σ\sigma be the Schnirelmann density. Then

σ(D+E)  ≥  σ(D)+σ(E)−σ(D) σ(E),\sigma(D+E) \;\ge\; \sigma(D)+\sigma(E)-\sigma(D)\,\sigma(E),

where D+E={d+e:d∈D, e∈E}D+E=\{d+e: d\in D,\ e\in E\}.

This is Schnirelmann's classical additive inequality, equivalently 1−σ(D+E)≤(1−σ(D))(1−σ(E))1-\sigma(D+E)\le(1-\sigma(D))(1-\sigma(E)). It applies to any sets containing 00 and is not specific to primes.

Formalization Note σ\sigma is Mathlib's schnirelmannDensity, with classical decidability. D+ED+E is the pointwise sumset.

Preamble
import Mathlib
import Definitions.Def_Schnir_defs
Formal statement
namespace Schnir

open Pointwise Classical in
theorem schnirelmann_ineq (D E : Set ℕ) (hD : 0 ∈ D) (hE : 0 ∈ E) :
    schnirelmannDensity D + schnirelmannDensity E
      - schnirelmannDensity D * schnirelmannDensity E ≤ schnirelmannDensity (D + E) := by sorry

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

View graph