Generalized logarithmic integral asymptotic

Proved

AsymptoticNumberTheory.logarithmicIntegral_isEquivalent

by elem · Oct 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysisanalytic-number-theoryasymptotics

For every positive integer $k$ , the generalized offset logarithmic integral satisfies

\int_2^x\frac{dt}{(\log t)^k}\sim\frac{x}{(\log x)^k}\qquad(x\to\infty).

The lower endpoint is $2$ , so the integrand has no logarithmic singularity on the intervals relevant to the limit. This classical analytic result converts integral prime-counting main terms into elementary ones and is independent of any prime-distribution conjecture.

This node records Lemma 2.3.2 of the source; its Lean proof remains a separate obligation.

Preamble

import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Mathlib.Analysis.Asymptotics.AsymptoticEquivalent

open Filter Topology Asymptotics

Formal statement

theorem AsymptoticNumberTheory.logarithmicIntegral_isEquivalent
    (k : ℕ) (hk : 0 < k) :
    (fun x : ℝ => ∫ t in (2 : ℝ)..x, (1 : ℝ) / (Real.log t) ^ k) ~[atTop]
      (fun x : ℝ => x / (Real.log x) ^ k) := by sorry

Source

S. L. Aletheia-Zomlefer, L. Fukshansky and S. R. Garcia, The Bateman-Horn conjecture: Heuristics, History, and Applications, https://www1.cmc.edu/pages/faculty/lenny/papers/bateman-horn.pdf; Lemma 2.3.2 and its proof, p. 4.

View graph