Li(2) Bounds - Lightweight Interface

This file provides the lightweight interface for li(2) bounds. It contains:

• Definitions of g(t) and li(2)
• Analytic lemmas (g_tendsto_one, g_bounded, g_pos, g_le_two, etc.)
• Statements of the certified bounds (proven in Li2Verified.lean)

Purpose

This module is designed to be fast to compile (~seconds) and is what downstream projects like PNT+ should import. The heavy numerical verification that proves the bounds is in Li2Verified.lean, which takes ~20 minutes but is only needed for LeanCert's CI, not for users of the bounds.

Main Results

• g - The symmetric log combination g(t) = 1/log(1+t) + 1/log(1-t)
• li2 - Definition of li(2) as ∫₀¹ g(t) dt
• g_tendsto_one - g(t) → 1 as t → 0⁺ (removable singularity)
• g_bounded - |g(t)| ≤ 2 for t ∈ (0, 1/2)
• g_pos, g_le_two - Positivity and upper bound on (0, 1)
• li2_lower - Lower bound: 1.039 ≤ li(2)
• li2_upper - Upper bound: li(2) ≤ 1.06

Verification Status

The bounds li2_lower and li2_upper are marked with sorry in this file. They are fully verified via interval arithmetic in Li2Verified.lean. This separation allows downstream projects to use the bounds without incurring the ~20 minute compilation cost of numerical verification.

Core Definitions

noncomputable def Li2.g (t : ℝ) : ℝ

The symmetric log combination g(t) = 1/log(1+t) + 1/log(1-t). This is the integrand for computing li(2).

Equations

• Li2.g t = LeanCert.Engine.TaylorModel.symmetricLogCombination t

noncomputable def Li2.li2 : ℝ

li(2) defined as the integral of the symmetric combination on [0, 1]. This is equivalent to the principal value integral ∫₀² dt/log(t).

Equations

• Li2.li2 = ∫ (t : ℝ) in 0..1, Li2.g t

Basic Properties

theorem Li2.g_eq (t : ℝ) : g t = 1 / Real.log (1 + t) + 1 / Real.log (1 - t)

The integrand g(t) equals 1/log(1+t) + 1/log(1-t)

theorem Li2.g_alt (t : ℝ) (ht_pos : 0 < t) (ht_lt : t < 1) : g t = Real.log (1 - t ^ 2) / (Real.log (1 + t) * Real.log (1 - t))

g(t) has an alternative form: log(1-t²)/(log(1+t)·log(1-t))

theorem Li2.g_tendsto_one : Filter.Tendsto g (nhdsWithin 0 (Set.Ioi 0)) (nhds 1)

g(t) → 1 as t → 0⁺ (the removable singularity)

theorem Li2.g_bounded (t : ℝ) (ht_pos : 0 < t) (ht_le : t < 1 / 2) : |g t| ≤ 2

|g(t)| ≤ 2 for t ∈ (0, 1/2]

Positivity and Global Upper Bound

theorem Li2.g_pos (t : ℝ) (ht_pos : 0 < t) (ht_lt : t < 1) : 0 < g t

g(t) > 0 for t ∈ (0, 1).

theorem Li2.g_le_two (t : ℝ) (ht_pos : 0 < t) (ht_lt : t < 1) : g t ≤ 2

g(t) ≤ 2 for t ∈ (0, 1).

Integrability

theorem Li2.g_intervalIntegrable_full : IntervalIntegrable g MeasureTheory.volume 0 1

g is integrable on [0, 1].

theorem Li2.g_intervalIntegrable (a b : ℝ) (ha_pos : 0 < a) (hb_lt : b < 1) (hab : a ≤ b) : IntervalIntegrable g MeasureTheory.volume a b

g is integrable on any closed subinterval of (0, 1).

Crude Bounds (Analytic)

theorem Li2.li2_upper_crude : li2 ≤ 2

Crude upper bound: li(2) ≤ 2. This follows from g(t) ≤ 2 on (0, 1).

theorem Li2.li2_pos : 0 < li2

li(2) > 0.

Certified Bounds

The following bounds are proven via interval arithmetic in Li2Verified.lean. They are stated here with sorry to allow downstream projects to use them without incurring the ~20 minute compilation cost of numerical verification.

The actual verification uses:

• Partition of [0, 1] into 7 subintervals
• Taylor model integration with 3000 partitions on [1/1000, 999/1000]
• Analytic bounds on tail intervals near 0 and 1

Sum of verified lower bounds: 1.03951 > 1.039 Sum of verified upper bounds: 1.0524 < 1.06

theorem Li2.li2_lower : ↑1039 / 1000 ≤ li2

Certified lower bound: li(2) ≥ 1.039. Proven via interval arithmetic in Li2Verified.lean.

theorem Li2.li2_upper : li2 ≤ ↑106 / 100

Certified upper bound: li(2) ≤ 1.06. Proven via interval arithmetic in Li2Verified.lean.

theorem Li2.li2_bounds : ↑1039 / 1000 ≤ li2 ∧ li2 ≤ ↑106 / 100

Combined bounds: li(2) ∈ [1.039, 1.06].

theorem Li2.li2_approx_1045 : |li2 - ↑1045 / 1000| ≤ ↑15 / 1000

li(2) is approximately 1.045 (the Ramanujan-Soldner constant). Our bounds show: |li(2) - 1.045| ≤ 0.015