Taylor Models - log(1+x) and Related Functions

This file contains Taylor polynomial definitions and remainder bounds for log(1+x) centered at 0, which is essential for handling principal value integrals like li(x).

Main definitions

• log1pTaylorPoly - Taylor polynomial for log(1+x) at center 0
• log1pRemainderBound - Remainder bound using Lagrange form
• tmLog1p - Function-level Taylor model
• tmLog1p_correct - Correctness theorem

Application: Bounds for the Logarithmic Integral li(x)

The symmetric combination g(t) = 1/log(1+t) + 1/log(1-t) appears in the principal value integral for li(x). Despite each term having a singularity at t=0, the combination is bounded. This file provides the infrastructure to prove this.

Key identity: g(t) = [log(1-t) + log(1+t)] / [log(1+t) · log(1-t)] = log(1-t²) / [log(1+t) · log(1-t)]

Using Taylor: log(1±t) ≈ ±t - t²/2 ∓ ... Numerator: log(1-t²) = -t² + O(t⁴) Denominator: log(1+t)·log(1-t) = -t² + O(t³) Therefore: g(t) → 1 as t → 0

log(1+x) Taylor polynomial

log(1+x) = x - x²/2 + x³/3 - x⁴/4 + ... = ∑_{k=1}^∞ (-1)^(k+1) x^k / k

Converges for x ∈ (-1, 1].

def LeanCert.Engine.TaylorModel.log1pTaylorCoeffs (n : ℕ) : ℕ → ℚ

Taylor polynomial coefficients for log(1+x) at center 0: For k ≥ 1: coeff_k = (-1)^(k+1) / k For k = 0: coeff_0 = 0 (since log(1+0) = 0)

Equations

• LeanCert.Engine.TaylorModel.log1pTaylorCoeffs n i = if i = 0 then 0 else if i ≤ n then (-1) ^ (i + 1) / ↑i else 0

noncomputable def LeanCert.Engine.TaylorModel.log1pTaylorPoly (n : ℕ) : Polynomial ℚ

Taylor polynomial for log(1+x) of degree n

Equations

• LeanCert.Engine.TaylorModel.log1pTaylorPoly n = ∑ i ∈ Finset.range (n + 1), Polynomial.C (LeanCert.Engine.TaylorModel.log1pTaylorCoeffs n i) * Polynomial.X ^ i

noncomputable def LeanCert.Engine.TaylorModel.log1pLagrangeRemainder (domain : Core.IntervalRat) (n : ℕ) : ℚ

Lagrange remainder bound for log(1+x) Taylor series centered at 0. The (n+1)th derivative of log(1+x) is (-1)^n · n! / (1+x)^(n+1). For the Taylor expansion at center 0, ξ lies between 0 and z:

• If z ≥ 0: ξ ∈ [0, z], so min(1+ξ) = 1
• If z < 0: ξ ∈ [z, 0], so min(1+ξ) = 1+z ≥ 1+lo Overall minimum is min(1, 1+lo). |R_n(x)| ≤ |x|^(n+1) / [(n+1) · min(1, 1+lo)^(n+1)]

Equations

• One or more equations did not get rendered due to their size.

theorem LeanCert.Engine.TaylorModel.log1pLagrangeRemainder_nonneg (domain : Core.IntervalRat) (n : ℕ) (hdom : domain.lo > -1) : 0 ≤ log1pLagrangeRemainder domain n

Remainder bound is nonnegative for valid domains

noncomputable def LeanCert.Engine.TaylorModel.tmLog1p (J : Core.IntervalRat) (n : ℕ) : Option TaylorModel

Taylor model for log(1+z) on domain J, centered at 0, degree n. Requires J.lo > -1 (domain must be in (-1, ∞)).

Equations

• One or more equations did not get rendered due to their size.

Correctness theorem

theorem LeanCert.Engine.TaylorModel.iteratedDeriv_log1p {n : ℕ} (hn : n ≠ 0) {y : ℝ} (hy : -1 < y) : iteratedDeriv n (fun (x : ℝ) => Real.log (1 + x)) y = (-1) ^ (n - 1) * ↑(n - 1).factorial * (1 + y) ^ (-↑n)

The n-th iterated derivative of log(1+x) at a point y > -1. Uses chain rule: since (1+x)' = 1, we have iteratedDeriv n (log ∘ (1+·)) y = iteratedDeriv n log (1+y). Combined with iteratedDeriv_log, this gives (-1)^(n-1) * (n-1)! * (1+y)^(-n).

theorem LeanCert.Engine.TaylorModel.iteratedDeriv_log1p_zero {n : ℕ} (hn : n ≠ 0) : iteratedDeriv n (fun (x : ℝ) => Real.log (1 + x)) 0 = (-1) ^ (n - 1) * ↑(n - 1).factorial

At x = 0, the n-th derivative of log(1+x) is (-1)^(n-1) * (n-1)!.

theorem LeanCert.Engine.TaylorModel.log1pTaylorCoeffs_eq_deriv (n i : ℕ) (hi_pos : 0 < i) (hi_le : i ≤ n) : ↑(log1pTaylorCoeffs n i) = iteratedDeriv i (fun (x : ℝ) => Real.log (1 + x)) 0 / ↑i.factorial

The coefficients of log1pTaylorPoly match the Taylor coefficients of log(1+x).

theorem LeanCert.Engine.TaylorModel.log1pTaylorPoly_aeval_eq_sum (n : ℕ) (z : ℝ) : (Polynomial.aeval z) (Polynomial.map (algebraMap ℚ ℝ) (log1pTaylorPoly n)) = ∑ i ∈ Finset.range (n + 1), iteratedDeriv i (fun (x : ℝ) => Real.log (1 + x)) 0 / ↑i.factorial * z ^ i

The polynomial evaluation of log1pTaylorPoly equals the Taylor sum.

theorem LeanCert.Engine.TaylorModel.log1p_taylor_remainder_bound (J : Core.IntervalRat) (n : ℕ) (z : ℝ) (hdom : J.lo > -1) (hz : z ∈ J) : |Real.log (1 + z) - (Polynomial.aeval z) (Polynomial.map (algebraMap ℚ ℝ) (log1pTaylorPoly n))| ≤ ↑(log1pLagrangeRemainder J n)

The Taylor remainder for log(1+x) at center 0 is bounded by the Lagrange form. This follows the standard Lagrange remainder bound proof:

• log(1+x) is C^∞ on (-1, ∞)
• The (n+1)th derivative is ±n!/(1+x)^(n+1)
• Apply taylor_remainder_bound_on to get the bound

theorem LeanCert.Engine.TaylorModel.tmLog1p_correct (J : Core.IntervalRat) (n : ℕ) (tm : TaylorModel) (h : tmLog1p J n = some tm) (z : ℝ) : z ∈ J → Real.log (1 + z) ∈ tm.evalSet z

log(1+z) ∈ (tmLog1p J n).evalSet z for all z in J when J.lo > -1.

Symmetric combination bound for li(x)

The key insight: g(t) = 1/log(1+t) + 1/log(1-t) is bounded for t ∈ (0, 1).

Algebraically: g(t) = [log(1-t) + log(1+t)] / [log(1+t) · log(1-t)] = log(1-t²) / [log(1+t) · log(1-t)]

Using Taylor expansions: log(1+t) = t - t²/2 + t³/3 - ... log(1-t) = -t - t²/2 - t³/3 - ... log(1-t²) = -t² - t⁴/2 - t⁶/3 - ...

Numerator: log(1-t²) = -t² · (1 + t²/2 + t⁴/3 + ...) Denominator: log(1+t) · log(1-t) = (t - t²/2 + ...)(-t - t²/2 - ...) = -t² + t⁴/4 + ... = -t² · (1 - t²/4 - ...)

So g(t) = [-t² · (1 + O(t²))] / [-t² · (1 + O(t²))] = 1 + O(t²)

More precisely: g(t) = [1 + t²/2 + O(t⁴)] / [1 - t²/4 + O(t⁴)] → 1 as t → 0

noncomputable def LeanCert.Engine.TaylorModel.symmetricLogCombination (t : ℝ) : ℝ

The symmetric combination g(t) = 1/log(1+t) + 1/log(1-t). This is well-defined for t ∈ (0, 1) despite the apparent singularity at t = 0.

Equations

• LeanCert.Engine.TaylorModel.symmetricLogCombination t = 1 / Real.log (1 + t) + 1 / Real.log (1 - t)

theorem LeanCert.Engine.TaylorModel.symmetricLogCombination_alt (t : ℝ) (ht_pos : 0 < t) (ht_lt : t < 1) : symmetricLogCombination t = Real.log (1 - t ^ 2) / (Real.log (1 + t) * Real.log (1 - t))

Alternative form: g(t) = log(1-t²) / (log(1+t) · log(1-t))

theorem LeanCert.Engine.TaylorModel.tendsto_log_one_add_div_self : Filter.Tendsto (fun (t : ℝ) => Real.log (1 + t) / t) (nhdsWithin 0 (Set.Ioi 0)) (nhds 1)

Helper: log(1+t)/t → 1 as t → 0. This follows from log'(1) = 1.

theorem LeanCert.Engine.TaylorModel.tendsto_log_one_sub_div_self : Filter.Tendsto (fun (t : ℝ) => Real.log (1 - t) / t) (nhdsWithin 0 (Set.Ioi 0)) (nhds (-1))

Helper: log(1-t)/t → -1 as t → 0⁺.

theorem LeanCert.Engine.TaylorModel.tendsto_log_one_sub_sq_div_sq : Filter.Tendsto (fun (t : ℝ) => Real.log (1 - t ^ 2) / t ^ 2) (nhdsWithin 0 (Set.Ioi 0)) (nhds (-1))

Helper: log(1-t²)/t² → -1 as t → 0⁺.

theorem LeanCert.Engine.TaylorModel.symmetricLogCombination_tendsto_one : Filter.Tendsto symmetricLogCombination (nhdsWithin 0 (Set.Ioi 0)) (nhds 1)

The limit as t → 0⁺ of g(t) is 1.

Proof using the key identity and limits: g(t) = log(1-t²) / (log(1+t) · log(1-t)) = [log(1-t²)/t²] / [(log(1+t)/t) · (log(1-t)/t)]

As t → 0⁺:

• log(1-t²)/t² → -1
• log(1+t)/t → 1
• log(1-t)/t → -1

So g(t) → (-1) / (1 · (-1)) = 1

theorem LeanCert.Engine.TaylorModel.symmetricLogCombination_bounded (t : ℝ) (ht_pos : 0 < t) (ht_lt : t < 1 / 2) : |symmetricLogCombination t| ≤ 2

Symmetric combination bound: |g(t)| ≤ C for t ∈ (0, δ) where δ < 1.

For small t, using Taylor analysis: g(t) = 1 + t²/2 · (1/log(1-t²) - 1/log(1+t) - 1/log(1-t)) + O(t⁴)

A crude but sufficient bound: for t ∈ (0, 1/2), |g(t)| ≤ 2. This can be refined using Taylor model arithmetic.

Summary of proven results for the li(2) computation

All proofs complete (no sorry):

• log1pTaylorPoly_aeval_eq_sum: Polynomial evaluation equals Taylor sum
• log1p_taylor_remainder_bound: Taylor remainder is bounded by Lagrange form
• tmLog1p_correct: Taylor model correctness for log(1+x)
• symmetricLogCombination_alt: g(t) = log(1-t²)/(log(1+t)·log(1-t))
• tendsto_log_one_add_div_self: log(1+t)/t → 1 as t → 0⁺
• tendsto_log_one_sub_div_self: log(1-t)/t → -1 as t → 0⁺
• tendsto_log_one_sub_sq_div_sq: log(1-t²)/t² → -1 as t → 0⁺
• symmetricLogCombination_tendsto_one: g(t) → 1 as t → 0⁺ (KEY RESULT)
• symmetricLogCombination_bounded: |g(t)| ≤ 2 for t ∈ (0, 1/2]
  • Case 1: near 0, uses continuity and limit → 1
  • Case 2: on [ε, 1/2], uses log bounds: log(1+t) ≥ t/(1+t), -log(1-t) ≤ t/(1-t)

The key insight for the li(2) computation is symmetricLogCombination_tendsto_one: the symmetric combination g(t) = 1/log(1+t) + 1/log(1-t) has a REMOVABLE SINGULARITY at t=0, with limit 1. This makes the principal value integral for li(2) = ∫₀¹ g(t) dt absolutely convergent.