Counting functions: constellations and primes below a bound
DefinitionHardyLittlewood_countingnumber-theoryprime-constellationsprime-counting
The counting layer of the Hardy–Littlewood conjectures. For a tuple of offsets m, the counting function π_P(n) returns the number of admissible prime constellations (p, p + 2m₁, ..., p + 2m_k) whose base point p is at most n. The prime-counting function π(n) returns the number of primes at most n. The second Hardy–Littlewood conjecture for a pair (x, y) is the subadditivity claim π(x + y) ≤ π(x) + π(y). Both counting functions are defined as the cardinalities of the corresponding finite sets of natural numbers.
Definition code
import Mathlib
import Definitions.Def_HardyLittlewood_constellation
namespace HardyLittlewood
/-- π_P(n): the number of admissible prime constellations
(p, p + 2·m₁, ..., p + 2·m_k) whose base point p is at most n. -/
noncomputable def primeTupleCounting {k : ℕ} (m : Fin k.succ → ℕ) (n : ℕ) : ℕ :=
{p : ℕ | p ≤ n ∧ IsAdmissiblePrimeConstellation m p}.ncard
/-- π(n): the prime-counting function — the number of primes at most n. -/
noncomputable def primeCounting (n : ℕ) : ℕ :=
{p : ℕ | p ≤ n ∧ p.Prime}.ncard
/-- The second Hardy–Littlewood conjecture for the pair (x, y):
π(x + y) ≤ π(x) + π(y). -/
def secondHardyLittlewoodFor (x y : ℕ) : Prop :=
primeCounting (x + y) ≤ primeCounting x + primeCounting y
end HardyLittlewood
Source
Formal Conjectures (2025), HardyLittlewood.lean, definitions Nat.primeTupleCounting and SecondHardyLittlewoodConjectureFor; the counting functions of Hardy and Littlewood (1923), Acta Math. 44
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.