Logarithmic integral $\mathrm{Li}$ and its inverse

Definition

LandauFunction_logIntegral

by Lucas · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

logarithmic-integralprime-number-theorem

The (offset) logarithmic integral is

\mathrm{Li}(x)=\int_2^x\frac{dt}{\ln t}\qquad(x\ge 2).

It is continuous and strictly increasing on $[2,\infty)$ , with $\mathrm{Li}(2)=0$ and $\mathrm{Li}(x)\to\infty$ , so it has an inverse $\mathrm{Li}^{-1}:[0,\infty)\to[2,\infty)$ . These functions appear in the prime number theorem and in the refined asymptotics of Landau's function.

Formalization Note logIntegral x is the interval integral $\int_2^x dt/\ln t$ (for $x<2$ it is the oriented integral). logIntegralInv y is defined as $\inf\{x\ge2:\ y\le\mathrm{Li}(x)\}$ , which equals $\mathrm{Li}^{-1}(y)$ for every $y\ge0$ (and is $2$ for $y<0$ ).

Definition code

import Mathlib

namespace LandauFunction

/-- The (offset) logarithmic integral `Li(x) = ∫₂ˣ dt / ln t`. -/
noncomputable def logIntegral (x : ℝ) : ℝ :=
  ∫ t in (2 : ℝ)..x, 1 / Real.log t

/-- The inverse `Li⁻¹` of the logarithmic integral: for `y ≥ 0`, the unique `x ≥ 2`
with `Li(x) = y` (realised as the least `x ≥ 2` with `y ≤ Li(x)`). -/
noncomputable def logIntegralInv (y : ℝ) : ℝ :=
  sInf {x : ℝ | 2 ≤ x ∧ y ≤ logIntegral x}

end LandauFunction

Source

Wikipedia, "Landau's function", revision oldid=1303222269 (https://en.wikipedia.org/w/index.php?title=Landau%27s_function&oldid=1303222269), paragraph "If π(x) − Li(x) = O(R(x)) …" (Li and Li⁻¹).

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — non-blind, same agent as the drafter

Non-blind read-back — not independent testimony. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statement below, with full knowledge of the source material and of the intended meaning. It is not a blind audit by an independent auditor, and no reviewer should treat it as independent evidence of faithfulness. It was produced at the explicit request of the proposal owner.

This file declares, inside the namespace LandauFunction, two real functions.

$\mathrm{Li}:\mathbb R\to\mathbb R$ (named logIntegral): for every real $x$ ,

\mathrm{Li}(x)=\int_2^x\frac{1}{\ln t}\,dt,

an oriented interval integral (so for $x<2$ it equals $-\int_x^2$ ). Here $\ln$ is the library's real logarithm, which satisfies $\ln 0=0$ and $\ln t=\ln|t|$ for $t<0$ , and $1/0=0$ . For $x\ge2$ the integrand is continuous and positive on $[2,x]$ and the value is the usual offset logarithmic integral, with $\mathrm{Li}(2)=0$ . For $1<x<2$ the value is $-\int_x^2 dt/\ln t$ . For $x\le1$ the interval contains $t=1$ , where $1/\ln t$ is not integrable, and the library then assigns the junk value $0$ to the integral.

$\mathrm{Li}^{-1}:\mathbb R\to\mathbb R$ (named logIntegralInv): for every real $y$ ,

\mathrm{Li}^{-1}(y)=\inf\{x\in\mathbb R:\ x\ge2\text{ and } y\le\mathrm{Li}(x)\},

the infimum of a set of reals in the library's convention (the infimum of an empty set is $0$ ). The set is bounded below by $2$ . For $y\le 0$ the point $x=2$ belongs to the set, so the value is $2$ . For $y>0$ the set is nonempty exactly when $\mathrm{Li}$ reaches $y$ on $[2,\infty)$ (true since $\mathrm{Li}(x)\to\infty$ ), and then, by continuity and strict monotonicity of $\mathrm{Li}$ on $[2,\infty)$ , the value is the unique $x\ge2$ with $\mathrm{Li}(x)=y$ ; these monotonicity and divergence facts are not stated in the file.

Human review

Endorsed by Shuze Chen · Oct 10, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 10, 2026
Confirmed by the mission captain (proposal self-audit).
Endorsed by pitimespi · Nov 3, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Logarithmic integral Li\mathrm{Li}Li and its inverse

Logarithmic integral $\mathrm{Li}$ and its inverse