Logarithmic integral

AbbreviationDomain of the logarithmic integral#✓fully proved

The domain of the logarithmic integral is the set of real numbers \(x\) with \(x \ge 0\) and \(x \ne 1\).

The point \(1\) is excluded because \(1 / \log t\) is singular at \(t = 1\); the classical integral \(\int_0^x dt / \log t\) has no finite real value at \(x = 1\) and is understood as a Cauchy principal value for \(x \ne 1\).

abbrev LogarithmicIntegralDomain : Type :=
  { x : ℝ // 0 ≤ x ∧ x ≠ 1 }

Sources

• arXiv:2306.14073v1 and arXiv:2309.16007v1, classical li(x) := PV ∫₀ˣ dt/log t with lower limit 0 and principal value at t = 1.

Used by 3

Used byLogarithmic integral · The logarithmic integral below \(1\) · The logarithmic integral above \(1\)

DefinitionLogarithmic integral#✓fully proved

For a real number \(x\) in the domain of the logarithmic integral (that is, \(x \ge 0\) and \(x \ne 1\)), the logarithmic integral \(\mathrm{li}(x)\) is \(\mathrm{li}(x) = \int_0^x \frac{dt}{\log t}\) if \(x < 1\), and if \(x > 1\) it is

\[ \mathrm{li}(x) = \int_0^1 \Big(\frac{1}{\log(1-u)} + \frac{1}{\log(1+u)}\Big) du + \int_2^x \frac{dt}{\log t}. \]

The first integral in the second case is the Cauchy principal value \(\mathrm{PV}\int_0^2 \frac{dt}{\log t}\), rewritten by the substitutions \(t = 1 - u\) and \(t = 1 + u\), so that \(\mathrm{li}(x)\) is the principal value \(\mathrm{PV}\int_0^x \frac{dt}{\log t}\). In particular \(\mathrm{li}(0) = 0\).

noncomputable def logarithmicIntegral (x : LogarithmicIntegralDomain) : ℝ :=
  if x.val < 1 then
    ∫ t in (0 : ℝ)..x.val, (Real.log t)⁻¹
  else
    (∫ u in (0 : ℝ)..(1 : ℝ), ((Real.log (1 - u))⁻¹ + (Real.log (1 + u))⁻¹)) +
      ∫ t in (2 : ℝ)..x.val, (Real.log t)⁻¹

Sources

• arXiv:2306.14073v1 and arXiv:2309.16007v1, normalized lower limit 0 and Cauchy principal value at t = 1 via symmetric pairing.

Uses 1 · Used by 5

Statement usesDomain of the logarithmic integral

Used byDerivative of the logarithmic integral · The logarithmic integral below \(1\) · The logarithmic integral above \(1\) · Real logarithmic integral extended by zero · The logarithmic integral vanishes at zero

TheoremThe logarithmic integral vanishes at zero#✓fully proved

The logarithmic integral \(\mathrm{li}\) satisfies \(\mathrm{li}(0) = 0\); here \(0\) lies in its domain since \(0 \ge 0\) and \(0 \ne 1\).

@[simp]
theorem logarithmicIntegral_zero {hx : 0 ≤ (0 : ℝ) ∧ (0 : ℝ) ≠ (1 : ℝ)} :
    logarithmicIntegral ⟨(0 : ℝ), hx⟩ = 0

Sources

• ∫₀⁰ = 0 for Lebesgue interval integrals; holds for any domain proof hx with x = 0.

Uses 1

Statement usesLogarithmic integral

TheoremThe logarithmic integral below \(1\)#✓fully proved

For every real number \(x\) with \(0 \le x < 1\), the logarithmic integral \(\mathrm{li}\) satisfies \(\mathrm{li}(x) = \int_0^x \frac{dt}{\log t}\).

theorem logarithmicIntegral_of_lt_one {x : LogarithmicIntegralDomain} (hx : x.val < 1) :
    logarithmicIntegral x = ∫ t in (0 : ℝ)..x.val, (Real.log t)⁻¹

Sources

• Direct unfolding of the x < 1 branch of the piecewise definition.

Uses 2 · Used by 1

Statement usesDomain of the logarithmic integral · Logarithmic integral

Used byDerivative of the logarithmic integral

TheoremThe logarithmic integral above \(1\)#✓fully proved

For every real number \(x > 1\), the logarithmic integral \(\mathrm{li}\) satisfies

\[ \mathrm{li}(x) = \int_0^1 \Big(\frac{1}{\log(1-u)} + \frac{1}{\log(1+u)}\Big) du + \int_2^x \frac{dt}{\log t}. \]

The paired integral over \([0, 1]\) is the symmetric principal value \(\mathrm{PV}\int_0^2 \frac{dt}{\log t}\).

theorem logarithmicIntegral_of_one_lt {x : LogarithmicIntegralDomain} (hx : 1 < x.val) :
    logarithmicIntegral x =
      (∫ u in (0 : ℝ)..(1 : ℝ), ((Real.log (1 - u))⁻¹ + (Real.log (1 + u))⁻¹)) +
        ∫ t in (2 : ℝ)..x.val, (Real.log t)⁻¹

Sources

• Direct unfolding of the x > 1 branch; ¬ x < 1 from 1 < x.

Uses 2 · Used by 1

Statement usesDomain of the logarithmic integral · Logarithmic integral

Used byDerivative of the logarithmic integral

DefinitionReal logarithmic integral extended by zero#✓fully proved

This is the function \(\mathbb{R} \to \mathbb{R}\) whose value at \(x\) is the logarithmic integral \(\operatorname{li}(x)\) when \(0 \le x\) and \(x \ne 1\), and \(0\) when \(x < 0\) or \(x = 1\).

The value \(0\) off the domain of \(\operatorname{li}\) is a convention. Near every \(x > 0\) with \(x \ne 1\) the function agrees with \(\operatorname{li}\), so its derivative there does not depend on this choice.

noncomputable def logarithmicIntegralReal (x : ℝ) : ℝ :=
  if h : 0 ≤ x ∧ x ≠ 1 then
    Real.logarithmicIntegral (⟨x, h⟩ : Real.LogarithmicIntegralDomain)
  else
    0

Uses 1 · Used by 6

Statement usesLogarithmic integral

Used byDerivative of the logarithmic integral · Tails of prime power sums from a Chebyshev bound · Tails of prime power sums under the Riemann hypothesis · The Mertens remainder from a Chebyshev bound · Johnston's range for Schoenfeld's inequality · Büthe's bound of the prime-counting function by the logarithmic integral

TheoremDerivative of the logarithmic integral#✓fully proved

For every real \(x\) with \(0 < x\) and \(x \ne 1\), the real logarithmic integral extended by zero has derivative \(1/\log x\) at \(x\).

Below \(1\) the function agrees near \(x\) with \(\int_0^x dt/\log t\); above \(1\) it agrees near \(x\) with the paired principal-value constant plus \(\int_2^x dt/\log t\). In both cases the fundamental theorem of calculus gives the derivative \(1/\log x\).

theorem hasDerivAt_logarithmicIntegralReal {x : ℝ}
    (hx_pos : 0 < x) (hx_ne_one : x ≠ 1) :
    HasDerivAt Real.logarithmicIntegralReal (1 / Real.log x) x

Uses 4

Statement usesReal logarithmic integral extended by zero

Proof usesLogarithmic integral · The logarithmic integral below \(1\) · The logarithmic integral above \(1\)

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.