The integral ∫₀¹ log²(x/(1 + x))/(1 + x²) dx

This file proves ∫₀¹ (log x - log(1 + x))²/(1 + x²) dx = 2 G log 2 + 2 Im Li₃((1+i)/2), the integral 𝒥 of A014, with an explicit primitive in the point χ(x) = x (1 - i)/(1 + x), which satisfies |χ(x)| = √2 x/(1 + x) ≤ 1/√2 on [0, 1].

Main results

• LeanPolyLog.Trilog.hasDerivAt_primJ: on (0, 1), with L(x) = log x - log(1 + x), primJ = L² log(1 - χ) + 2 L Li₂(χ) - 2 Li₃(χ) has derivative L² (1/(x - i) - 1/(x + 1)), whose imaginary part is L²/(1 + x²).
• LeanPolyLog.Trilog.continuousOn_primJ: primJ is continuous on [0, 1], including at 0, where L is unbounded.
• LeanPolyLog.Trilog.integral_log_sub_log_sq_div_one_add_sq: the value of the integral.

Proof sketch

• χ'/χ = 1/x - 1/(1 + x) = L', which makes the Li₂ and Li₃ terms cancel in the derivative, and -χ'/(1 - χ) = 1/(x - i) - 1/(x + 1). This is the substitution u = x/(1 + x) of the tutorial, done inside the primitive.
• Continuity at 0: Li_s(z) = z ∑ zⁿ/(n+1)^s (LeanPolyLog.Trilog.Li_eq_mul_tsum) and log(1 - z) = -Li₁(z). So L² log(1 - χ) and L Li₂(χ) are x L² and x L times functions that are continuous because |χ| ≤ 3/4. Both x L² and x L are continuous at 0.
• The integrand is nonnegative, so it is integrable (intervalIntegral.integrableOn_deriv_of_nonneg). Then primJ 0 = 0, and Im primJ 1 = (π/4) log² 2 - 2 log 2 Im Li₂((1-i)/2) - 2 Im Li₃((1-i)/2).

The point χ(x)

noncomputable def LeanPolyLog.Trilog.chi (x : ℝ) : ℂ

χ(x) = x (1 - i)/(1 + x).

Equations

• LeanPolyLog.Trilog.chi x = ↑(x / (1 + x)) * (1 - Complex.I)

theorem LeanPolyLog.Trilog.chi_re (x : ℝ) : (chi x).re = x / (1 + x)

theorem LeanPolyLog.Trilog.normSq_chi (x : ℝ) : Complex.normSq (chi x) = 2 * (x / (1 + x)) ^ 2

|χ(x)|² = 2 (x/(1 + x))².

theorem LeanPolyLog.Trilog.norm_chi_le {x : ℝ} (hx : x ∈ Set.Icc 0 1) : ‖chi x‖ ≤ 3 / 4

On [0, 1], |χ(x)| ≤ 1/√2 < 3/4.

theorem LeanPolyLog.Trilog.norm_chi_lt_one {x : ℝ} (hx : x ∈ Set.Icc 0 1) : ‖chi x‖ < 1

theorem LeanPolyLog.Trilog.chi_ne_zero {x : ℝ} (hx : 0 < x) : chi x ≠ 0

theorem LeanPolyLog.Trilog.one_sub_chi_mem_slitPlane {x : ℝ} (hx : 0 ≤ x) : 1 - chi x ∈ Complex.slitPlane

For x ≥ 0, Re (1 - χ(x)) = 1/(1 + x) > 0.

theorem LeanPolyLog.Trilog.one_add_mul_I_ne_zero (x : ℝ) : 1 + ↑x * Complex.I ≠ 0

theorem LeanPolyLog.Trilog.one_sub_chi {x : ℝ} (hx : 0 ≤ x) : 1 - chi x = (1 + ↑x * Complex.I) / (1 + ↑x)

1 - χ(x) = (1 + x i)/(1 + x).

theorem LeanPolyLog.Trilog.chi_zero : chi 0 = 0

theorem LeanPolyLog.Trilog.chi_one : chi 1 = (1 - Complex.I) / 2

Derivatives

theorem LeanPolyLog.Trilog.hasDerivAt_chi {x : ℝ} (hx : 0 ≤ x) : HasDerivAt chi (↑(1 / (1 + x) ^ 2) * (1 - Complex.I)) x

theorem LeanPolyLog.Trilog.deriv_chi_div_chi {x : ℝ} (hx : 0 < x) : ↑(1 / (1 + x) ^ 2) * (1 - Complex.I) / chi x = ↑(1 / x - 1 / (1 + x))

χ'/χ = 1/x - 1/(1 + x).

theorem LeanPolyLog.Trilog.neg_deriv_chi_div_one_sub_chi {x : ℝ} (hx : 0 ≤ x) : -(↑(1 / (1 + x) ^ 2) * (1 - Complex.I)) / (1 - chi x) = 1 / (↑x - Complex.I) - 1 / (↑x + 1)

-χ'/(1 - χ) = 1/(x - i) - 1/(x + 1).

The primitive

noncomputable def LeanPolyLog.Trilog.primJ (x : ℝ) : ℂ

A primitive of L(x)² (1/(x - i) - 1/(x + 1)) on (0, 1), with L(x) = log x - log(1 + x): L² log(1 - χ) + 2 L Li₂(χ) - 2 Li₃(χ).

Equations

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

theorem LeanPolyLog.Trilog.hasDerivAt_primJ {x : ℝ} (hx0 : 0 < x) (hx1 : x < 1) : HasDerivAt primJ (↑(Real.log x - Real.log (1 + x)) ^ 2 * (1 / (↑x - Complex.I) - 1 / (↑x + 1))) x

On (0, 1), primJ' = L² (1/(x - i) - 1/(x + 1)).

theorem LeanPolyLog.Trilog.im_ofReal_mul_sub (a x : ℝ) : (↑a * (1 / (↑x - Complex.I) - 1 / (↑x + 1))).im = a / (1 + x ^ 2)

Im (a (1/(x - i) - 1/(x + 1))) = a/(1 + x²) for real a and x.

theorem LeanPolyLog.Trilog.hasDerivAt_im_primJ {x : ℝ} (hx0 : 0 < x) (hx1 : x < 1) : HasDerivAt (fun (t : ℝ) => (primJ t).im) ((Real.log x - Real.log (1 + x)) ^ 2 / (1 + x ^ 2)) x

On (0, 1), (Im primJ)' = (log x - log(1 + x))²/(1 + x²).

Continuity of the primitive at 0

theorem LeanPolyLog.Trilog.Li_eq_mul_tsum (s : ℕ) (z : ℂ) : Li s z = z * ∑' (n : ℕ), z ^ n / (↑n + 1) ^ s

Li_s(z) = z ∑ zⁿ/(n+1)^s.

theorem LeanPolyLog.Trilog.continuousOn_tsum_pow_div_succ_pow (s : ℕ) {r : ℝ} (hr0 : 0 ≤ r) (hr1 : r < 1) : ContinuousOn (fun (z : ℂ) => ∑' (n : ℕ), z ^ n / (↑n + 1) ^ s) (Metric.closedBall 0 r)

For 0 ≤ r < 1, z ↦ ∑ zⁿ/(n+1)^s is continuous on the closed ball of radius r (Weierstrass M-test with rⁿ).

theorem LeanPolyLog.Trilog.continuousOn_mul_log_sub_log : ContinuousOn (fun (t : ℝ) => t * (Real.log t - Real.log (1 + t))) (Set.Icc 0 1)

x ↦ x (log x - log(1 + x)) is continuous on [0, 1].

theorem LeanPolyLog.Trilog.continuousOn_mul_log_sub_log_sq : ContinuousOn (fun (t : ℝ) => t * (Real.log t - Real.log (1 + t)) ^ 2) (Set.Icc 0 1)

x ↦ x (log x - log(1 + x))² is continuous on [0, 1].

theorem LeanPolyLog.Trilog.continuousOn_chi : ContinuousOn chi (Set.Icc 0 1)

theorem LeanPolyLog.Trilog.continuousOn_primJ : ContinuousOn primJ (Set.Icc 0 1)

primJ is continuous on [0, 1]. On [0, 1] it equals -(x L²/(1 + x)) (1 - i) S₁(χ) + 2 (x L/(1 + x)) (1 - i) S₂(χ) - 2 Li₃(χ) with S_s(z) = ∑ zⁿ/(n+1)^s, and each factor is continuous there.

The integral

theorem LeanPolyLog.Trilog.intervalIntegrable_log_sub_log_sq_div_one_add_sq : IntervalIntegrable (fun (x : ℝ) => (Real.log x - Real.log (1 + x)) ^ 2 / (1 + x ^ 2)) MeasureTheory.volume 0 1

(log x - log(1 + x))²/(1 + x²) is integrable on [0, 1]: it is the nonnegative derivative of the continuous function Im primJ.

theorem LeanPolyLog.Trilog.integral_log_sub_log_sq_div_one_add_sq_eq : ∫ (x : ℝ) in 0..1, (Real.log x - Real.log (1 + x)) ^ 2 / (1 + x ^ 2) = (primJ 1).im - (primJ 0).im

∫₀¹ (log x - log(1 + x))²/(1 + x²) dx = Im primJ 1 - Im primJ 0.

theorem LeanPolyLog.Trilog.primJ_zero : primJ 0 = 0

theorem LeanPolyLog.Trilog.im_primJ_one : (primJ 1).im = 2 * G * Real.log 2 + 2 * (Li 3 ((1 + Complex.I) / 2)).im

Im primJ 1 = 2 G log 2 + 2 Im Li₃((1+i)/2).

theorem LeanPolyLog.Trilog.integral_log_sub_log_sq_div_one_add_sq : ∫ (x : ℝ) in 0..1, (Real.log x - Real.log (1 + x)) ^ 2 / (1 + x ^ 2) = 2 * G * Real.log 2 + 2 * (Li 3 ((1 + Complex.I) / 2)).im

∫₀¹ (log x - log(1 + x))²/(1 + x²) dx = 2 G log 2 + 2 Im Li₃((1+i)/2).