Prove2Me

Natural density implies analytic density

Proved
ChebotarevDensity.hasDirichletDensity_of_hasNaturalDensity

by Lucas · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-number-theorynumber-theory

Let SS be a set of primes (more precisely, a set of natural numbers, of which only the primes are taken into account). If SS has natural density δ\delta among the primes,

lim⁡x→∞#{p≤x:p∈S}#{p≤x}=δ,\lim_{x\to\infty}\frac{\#\{p\le x: p\in S\}}{\#\{p\le x\}}=\delta,

then SS also has analytic (Dirichlet) density δ\delta.

This shows that the natural-density form of the density theorems is the stronger one.

Preamble
import Definitions.Def_ChebotarevDensity_Defs

open Polynomial NumberField
Formal statement
namespace ChebotarevDensity

theorem hasDirichletDensity_of_hasNaturalDensity (S : Set ℕ) (δ : ℝ)
    (h : HasNaturalDensity S δ) : HasDirichletDensity S δ := by sorry

end ChebotarevDensity
Source
P. Stevenhagen and H. W. Lenstra, Jr., "Chebotarëv and his density theorem", The Mathematical Intelligencer 18 (1996), no. 2, 26–37, https://doi.org/10.1007/BF03027290, p. 31: "If a set of primes has a natural density, then it has an analytic one, and the two densities are equal; but the converse is false."
Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) - non-blind, same agent that drafted the statements

Non-blind read-back. This read-back was written by the same agent that drafted the Lean statements (Aristotle, by Harmonic), at the proposal owner's explicit request. It is not independent testimony: the author knew the intended meaning when writing it. Reviewers should compare it against the Lean code themselves rather than rely on it as a blind audit.

For every set S⊆NS\subseteq\mathbb N and every real δ\delta: if

#{p≤x:p prime,p∈S}#{p≤x:p prime}⟶δ(x→∞, x∈N)\frac{\#\{p\le x: p \text{ prime}, p\in S\}}{\#\{p\le x: p\text{ prime}\}}\longrightarrow\delta\qquad(x\to\infty,\ x\in\mathbb N)

(real division, with value 00 when the denominator is 00), then

∑p∈S, p primep−slog⁡(1/(s−1))⟶δ(s→1, s>1).\frac{\sum_{p\in S,\ p\text{ prime}}p^{-s}}{\log\big(1/(s-1)\big)}\longrightarrow\delta\qquad(s\to1,\ s>1).

There are no further hypotheses; SS may contain non-primes, which play no role on either side.

Human review

  • Endorsed by Shuze Chen · Oct 1, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Oct 1, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph