The logarithmic-integral model diverges
ProvedHardyLittlewood.tuple_integral_divergesFor every multiplicity k + 1, the model integral of the first Hardy–Littlewood conjecture grows without bound: the integral of 1/(log t)^(k+1) over [2, n] tends to +∞ as n → ∞. This is the divergence that makes the conjecture's conclusion an infinitude statement: a positive constant against a diverging model forces the count to grow.
import Mathlib import Definitions.Def_HardyLittlewood_constellation import Definitions.Def_HardyLittlewood_counting import Definitions.Def_HardyLittlewood_series
namespace HardyLittlewood
/-- The model integral of the first Hardy–Littlewood conjecture diverges: for
every multiplicity k + 1, the integral of 1 / (log t)^(k+1) over [2, n] grows
without bound as n → ∞. -/
theorem tuple_integral_diverges (k : ℕ) :
Filter.Tendsto (fun n => ∫ t in (2:ℝ)..(n:ℝ), 1 / (Real.log t) ^ (k + 1))
Filter.atTop Filter.atTop := 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, the function sending each natural number n to the integral from 2 to n of the function t ↦ 1 divided by the (k+1)-th power of the natural logarithm of t tends to positive infinity along the filter at top; that is, for every real bound there is an index beyond which all values of the function exceed the bound.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.