The logarithmic integral

This file defines the offset logarithmic integral Li x = ∫ t in 2..x, (log t)⁻¹ and proves the prime-number-theorem normalisation Li x ~ x / log x as x → ∞.

The lower endpoint is 2 rather than 0: the integrand has a nonintegrable singularity at t = 1, so the unshifted li exists only as a principal value, while every arithmetic application compares a prime count with Li. The endpoint agrees with the one used by the partial-summation identities for prime counts, so the two can be combined without a shift of origin.

The asymptotic is proved from the exact identity Li x = x / log x - 2 / log 2 + ∫ t in 2..x, ((log t) ^ 2)⁻¹, the fundamental theorem of calculus applied to t ↦ t / log t, together with the estimate that the remaining integral is o (x / log x). Splitting that integral at √x bounds it by √x / (log 2) ^ 2 + 4 * x / (log x) ^ 2, and both terms are o (x / log x).

Main declarations

• TauCeti.Real.logIntegral — the offset logarithmic integral.
• TauCeti.Real.le_logIntegral — the elementary lower bound (x - 2) / log x ≤ Li x.
• TauCeti.Real.logIntegral_eq_div_log_sub_add — the antiderivative identity above.
• TauCeti.Real.logIntegral_isEquivalent_div_log — Li x ~ x / log x at infinity, with the quotient form TauCeti.Real.tendsto_logIntegral_mul_log_div_atTop.
• TauCeti.Real.tendsto_div_div_log_of_isLittleO_logIntegral — an o (x / log x) error relative to δ Li x gives f x / (x / log x) → δ.
• TauCeti.Real.isLittleO_integral_div_mul_log_sq — for f interval integrable above 2 and of at most linear growth, ∫ t in 2..x, f t / (t * log t ^ 2) is o (x / log x).

The auxiliary bounds TauCeti.Real.integral_inv_log_pow_le and TauCeti.Real.le_integral_inv_log_pow estimate ∫ t in a..b, ((log t) ^ n)⁻¹ by monotonicity of the logarithm. They are stated for a general exponent because the identity above needs n = 2 while Li itself is the case n = 1.

Roadmap role

This is the analytic half of Layer 6.2 of TauCetiRoadmap/ArithmeticDirichletSeries/README.md, which asks for Li together with Li(x) ∼ x/log x on the way to the transfer ϑ(x) ∼ δx ⟹ π(x) ∼ δ Li(x) that Layer 10.3 exports as primeCount_asymptotic_of_primeTheta. The weighted-remainder estimate isLittleO_integral_div_mul_log_sq is the analytic input to that transfer: it is what absorbs the integral produced by Abel summation.

References

• H. Davenport, Multiplicative Number Theory, Chapter 1.
• G. Tenenbaum, Introduction to Analytic and Probabilistic Number Theory, Chapter I.

Mathlib's Mathlib/NumberTheory/Chebyshev.lean carries out this estimate for the rational Chebyshev function, in Chebyshev.integral_theta_div_log_sq_isLittleO; the argument for a general integrand below follows the same split into a bounded initial segment and a linearly bounded tail.

Reciprocal powers of the logarithm

theorem TauCeti.Real.continuousOn_inv_log_pow (n : ℕ) : ContinuousOn (fun (t : ℝ) => (Real.log t ^ n)⁻¹) (Set.Ioi 1)

Reciprocal powers of the logarithm are continuous to the right of its zero t = 1.

theorem TauCeti.Real.intervalIntegrable_inv_log_pow (n : ℕ) {a b : ℝ} (ha : 1 < a) (hb : 1 < b) : IntervalIntegrable (fun (t : ℝ) => (Real.log t ^ n)⁻¹) MeasureTheory.volume a b

Reciprocal powers of the logarithm are interval integrable on any interval to the right of 1.

theorem TauCeti.Real.integral_inv_log_pow_le (n : ℕ) {a b : ℝ} (ha : 1 < a) (hab : a ≤ b) : ∫ (t : ℝ) in a..b, (Real.log t ^ n)⁻¹ ≤ (b - a) / Real.log a ^ n

Monotonicity of the logarithm bounds ∫ t in a..b, (log t ^ n)⁻¹ above by the value of the integrand at the left endpoint.

theorem TauCeti.Real.le_integral_inv_log_pow (n : ℕ) {a b : ℝ} (ha : 1 < a) (hab : a ≤ b) : (b - a) / Real.log b ^ n ≤ ∫ (t : ℝ) in a..b, (Real.log t ^ n)⁻¹

Monotonicity of the logarithm bounds ∫ t in a..b, (log t ^ n)⁻¹ below by the value of the integrand at the right endpoint.

theorem TauCeti.Real.integral_inv_log_pow_nonneg (n : ℕ) {a b : ℝ} (ha : 1 < a) (hab : a ≤ b) : 0 ≤ ∫ (t : ℝ) in a..b, (Real.log t ^ n)⁻¹

The integrand (log t ^ n)⁻¹ is nonnegative to the right of 1, so its integral is.

The logarithmic integral

noncomputable def TauCeti.Real.logIntegral (x : ℝ) : ℝ

The offset logarithmic integral Li x = ∫ t in 2..x, (log t)⁻¹.

The lower endpoint 2 avoids the singularity of the integrand at t = 1; this is the function appearing in the prime number theorem in the form π x ~ Li x.

Equations

• TauCeti.Real.logIntegral x = ∫ (t : ℝ) in 2..x, (Real.log t)⁻¹

theorem TauCeti.Real.logIntegral_def (x : ℝ) : logIntegral x = ∫ (t : ℝ) in 2..x, (Real.log t)⁻¹

Defining equation of TauCeti.Real.logIntegral.

@[simp]

theorem TauCeti.Real.logIntegral_two : logIntegral 2 = 0

theorem TauCeti.Real.logIntegral_nonneg {x : ℝ} (hx : 2 ≤ x) : 0 ≤ logIntegral x

The logarithmic integral is nonnegative from its base point on.

theorem TauCeti.Real.le_logIntegral {x : ℝ} (hx : 2 ≤ x) : (x - 2) / Real.log x ≤ logIntegral x

The elementary lower bound (x - 2) / log x ≤ Li x, by monotonicity of the logarithm.

The asymptotic Li x ~ x / log x

theorem TauCeti.Real.hasDerivAt_div_log {t : ℝ} (ht : 1 < t) : HasDerivAt (fun (u : ℝ) => u / Real.log u) ((Real.log t)⁻¹ - (Real.log t ^ 2)⁻¹) t

The derivative of t ↦ t / log t to the right of 1.

theorem TauCeti.Real.logIntegral_eq_div_log_sub_add {x : ℝ} (hx : 2 ≤ x) : logIntegral x = x / Real.log x - 2 / Real.log 2 + ∫ (t : ℝ) in 2..x, (Real.log t ^ 2)⁻¹

The antiderivative identity for the logarithmic integral. Integrating the derivative of t ↦ t / log t from 2 to x writes Li x as x / log x plus a constant and a remainder integral, which the asymptotic below shows is o (x / log x).

theorem TauCeti.Real.tendsto_integral_inv_log_sq_mul_log_div_atTop : Filter.Tendsto (fun (x : ℝ) => (∫ (t : ℝ) in 2..x, (Real.log t ^ 2)⁻¹) * Real.log x / x) Filter.atTop (nhds 0)

The remainder integral of the antiderivative identity is o (x / log x).

theorem TauCeti.Real.tendsto_logIntegral_mul_log_div_atTop : Filter.Tendsto (fun (x : ℝ) => logIntegral x * Real.log x / x) Filter.atTop (nhds 1)

The logarithmic integral is asymptotic to x / log x, in quotient form.

theorem TauCeti.Real.logIntegral_isEquivalent_div_log : Asymptotics.IsEquivalent Filter.atTop logIntegral fun (x : ℝ) => x / Real.log x

Li x is asymptotically equivalent to x / log x.

A weighted remainder integral

The integral ∫ t in 2..x, f t / (t * log t ^ 2) is what Abel summation leaves behind when a logarithmically weighted counting function is converted into an unweighted one. It is negligible on the scale x / log x as soon as f grows at most linearly.

theorem TauCeti.Real.tendsto_div_log_atTop : Filter.Tendsto (fun (x : ℝ) => x / Real.log x) Filter.atTop Filter.atTop

The Chebyshev scale x / log x diverges. Equivalently, a constant is o (x / log x).

theorem TauCeti.Real.isLittleO_const_div_log (c : ℝ) : (fun (x : ℝ) => c) =o[Filter.atTop] fun (x : ℝ) => x / Real.log x

A constant is o (x / log x), because that scale diverges.

theorem TauCeti.Real.tendsto_div_div_log_of_isLittleO_logIntegral {f : ℝ → ℝ} {δ : ℝ} (h : (fun (x : ℝ) => f x - δ * logIntegral x) =o[Filter.atTop] fun (x : ℝ) => x / Real.log x) : Filter.Tendsto (fun (x : ℝ) => f x / (x / Real.log x)) Filter.atTop (nhds δ)

An error of o (x / log x) relative to δ Li x gives the ratio limit f x / (x / log x) → δ, since Li x ~ x / log x.

theorem TauCeti.Real.isLittleO_integral_inv_log_sq : (fun (x : ℝ) => ∫ (t : ℝ) in 2..x, (Real.log t ^ 2)⁻¹) =o[Filter.atTop] fun (x : ℝ) => x / Real.log x

∫ t in 2..x, (log t ^ 2)⁻¹ is o (x / log x); this is TauCeti.Real.tendsto_integral_inv_log_sq_mul_log_div_atTop read as an IsLittleO.

theorem TauCeti.Real.intervalIntegrable_div_mul_log_sq {f : ℝ → ℝ} {a b : ℝ} (ha : 1 < a) (hb : 1 < b) (hf : IntervalIntegrable f MeasureTheory.volume a b) : IntervalIntegrable (fun (t : ℝ) => f t / (t * Real.log t ^ 2)) MeasureTheory.volume a b

The weight (t * log t ^ 2)⁻¹ is continuous to the right of 1, so it preserves interval integrability there.

theorem TauCeti.Real.isLittleO_integral_div_mul_log_sq {f : ℝ → ℝ} (hf_int : ∀ (x : ℝ), 2 ≤ x → IntervalIntegrable f MeasureTheory.volume 2 x) (hf : f =O[Filter.atTop] id) : (fun (x : ℝ) => ∫ (t : ℝ) in 2..x, f t / (t * Real.log t ^ 2)) =o[Filter.atTop] fun (x : ℝ) => x / Real.log x

A linearly bounded integrand leaves a negligible remainder. If f is interval integrable above 2 and satisfies f = O(x), then ∫ t in 2..x, f t / (t * log t ^ 2) is o (x / log x).

For the rational Chebyshev function this is Chebyshev.integral_theta_div_log_sq_isLittleO.