Positive prime-relative density implies infinitude

Proved

HorizontalPadicL.positiveDensityPrimeSet_infinite

by davidloeffler · Sep 19, 2026 · Mathlib 0df444a (Lean v4.33.1)

number-theoryprime-densityset-theory

Let $A$ be a set of natural numbers. Suppose that the proportion of rational primes below $X$ which belong to $A$ has a limit $\delta>0$ as $X\to\infty$ . Then $A$ is infinite.

Equivalently, if

\lim_{X\to\infty} \frac{\#\{\ell<X:\ \ell\text{ prime and }\ell\in A\}} {\#\{\ell<X:\ \ell\text{ prime}\}} =\delta>0,

then $A$ contains infinitely many natural numbers. This elementary consequence of positive density is useful whenever a density-defined prime set must be enumerated as an infinite sequence.

Preamble

import Definitions.Def_KN_HorizontalPadicLDensityExtension

set_option autoImplicit false

Formal statement

namespace HorizontalPadicL

/-- A set of natural numbers having positive natural density relative to the
rational primes is infinite. -/
theorem positiveDensityPrimeSet_infinite
    (A : Set ℕ) (δ : ℝ) (hδ : 0 < δ)
    (hdensity : HasPrimeNaturalDensity A δ) : A.Infinite := by sorry

end HorizontalPadicL

Source

Elementary consequence of prime-relative natural density; for the density convention used in the horizontal argument, see Kriz–Nordentoft, https://arxiv.org/pdf/2310.20678, Definition 4.1.

View graph