The first Hardy–Littlewood conjecture: prime constellations have logarithmic-integral density
OpenHardyLittlewood.first_hardy_littlewoodThe goal: for every tuple m with m₀ = 0 and pairwise distinct offsets, the counting function π_P(n) of admissible prime constellations with offsets m is asymptotic to C_P times the integral of 1/(log t)^(k+1) from 2 to n, where C_P is the singular series constant of the tuple. For the twin offsets this yields the twin prime conjecture; in general it is the prime k-tuple conjecture of 1923, the open heart of the mission.
import Mathlib import Definitions.Def_HardyLittlewood_constellation import Definitions.Def_HardyLittlewood_counting import Definitions.Def_HardyLittlewood_series
namespace HardyLittlewood
/-- The first Hardy–Littlewood conjecture: for every tuple m with m 0 = 0 and
pairwise distinct offsets, the counting function π_P(n) of admissible prime
constellations with offsets m and base point at most n is asymptotic to the
singular series constant C_P times the (k+1)-fold logarithmic integral from 2
to n. -/
theorem first_hardy_littlewood {k : ℕ} (m : Fin k.succ → ℕ) :
firstHardyLittlewoodFor m := by
sorry
end HardyLittlewood
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
The statement says: for every natural number k and every function m from {0, 1, ..., k} to the natural numbers, the first Hardy–Littlewood conjecture holds for m: whenever m evaluated at 0 is 0 and m is injective, the sequence whose value at n is the cardinality of the set of base points p at most n carrying an admissible prime constellation with offsets m, viewed as a real sequence, is asymptotic — in the sense that the difference is little-o of the model — to the sequence whose value at n is the singular-series constant of m times the integral from 2 to n of 1 divided by the (k+1)-th power of the natural logarithm.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.