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

This file proves ∫₀¹ log²(1 + x)/(1 + x²) dx = 7π³/64 + (3π/16) log² 2 - 2 G log 2 - 4 Im Li₃((1+i)/2), the integral ℳ of A014, using Li only on the closed unit disk.

The tutorial expands 1/(x - i) in powers of x/(1+i) on [1, 2], which diverges for x > √2, and arrives at Li₃(1+i), outside the disk. Instead we use an explicit primitive built from the two points

• ψ(x) = ((1 - x) + (1 + x) i)/2, with |ψ(x)|² = (1 + x²)/2, and
• φ(x) = (x - i)/(x + 1) = ψ(x)/(ψ(x) - 1), with |φ(x)|² = (1 + x²)/(1 + x)².

For x ∈ [0, 1] both lie in the closed unit disk, and for x ∈ (0, 1) in the open disk. The endpoints are ψ(0) = (1+i)/2, ψ(1) = i, φ(0) = -i and φ(1) = (1-i)/2.

Main results

• LeanPolyLog.Trilog.hasDerivAt_primM: on (0, 1), with μ = log((1 - i)/2), primM = μ² log ψ - 2 log(1 + x) Li₂(ψ) + 2 Li₃(φ) + 2 Li₃(ψ) - (log(1 + x) + μ)³/3 has derivative log²(1 + x)/(x - i).
• LeanPolyLog.Trilog.continuousOn_primM: primM is continuous on [0, 1].
• LeanPolyLog.Trilog.integral_log_one_add_sq_div_one_add_sq: the value of the integral.

Proof sketch

• ψ'/ψ = 1/(x - i) and φ'/φ = 1/(x - i) - 1/(x + 1), and 1 - ψ = (1 + x)(1 - i)/2, so log(1 - ψ) = log(1 + x) + μ.
• Landen's identity (LeanPolyLog.Dilog.Li_two_add_Li_two_div_sub_one, which applies because |ψ| ≤ 1 and Re ψ = (1 - x)/2 ≤ 1/2) gives Li₂(φ) = -Li₂(ψ) - ½ (log(1 + x) + μ)². With it, the derivative of primM collapses to log²(1 + x)/(x - i).
• Since Im (1/(x - i)) = 1/(1 + x²), the fundamental theorem of calculus applied to Im primM gives the integral as Im (primM 1 - primM 0), which is evaluated with Im Li₃(±i) = ±π³/32, Im Li₂(i) = G, Im Li₃((1-i)/2) = -Im Li₃((1+i)/2) and the logarithms of i and (1±i)/2.

The points ψ(x) and φ(x)

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

ψ(x) = ((1 - x) + (1 + x) i)/2.

Equations

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

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

φ(x) = (x - i)/(x + 1), which equals ψ(x)/(ψ(x) - 1).

Equations

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

theorem LeanPolyLog.Trilog.psi_re (x : ℝ) : (psi x).re = (1 - x) / 2

theorem LeanPolyLog.Trilog.psi_im (x : ℝ) : (psi x).im = (1 + x) / 2

theorem LeanPolyLog.Trilog.normSq_psi (x : ℝ) : Complex.normSq (psi x) = (1 + x ^ 2) / 2

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

theorem LeanPolyLog.Trilog.norm_psi_le_one {x : ℝ} (hx : |x| ≤ 1) : ‖psi x‖ ≤ 1

theorem LeanPolyLog.Trilog.norm_psi_lt_one {x : ℝ} (hx : |x| < 1) : ‖psi x‖ < 1

theorem LeanPolyLog.Trilog.psi_mem_slitPlane {x : ℝ} (hx : -1 < x) : psi x ∈ Complex.slitPlane

For x > -1, Im ψ(x) > 0, so ψ(x) is in the slit plane.

theorem LeanPolyLog.Trilog.psi_ne_zero {x : ℝ} (hx : -1 < x) : psi x ≠ 0

theorem LeanPolyLog.Trilog.ofReal_add_one_ne_zero {x : ℝ} (hx : -1 < x) : ↑x + 1 ≠ 0

theorem LeanPolyLog.Trilog.normSq_phi (x : ℝ) : Complex.normSq (phi x) = (x ^ 2 + 1) / (x + 1) ^ 2

|φ(x)|² = (x² + 1)/(x + 1)².

theorem LeanPolyLog.Trilog.norm_phi_le_one {x : ℝ} (hx : 0 ≤ x) : ‖phi x‖ ≤ 1

theorem LeanPolyLog.Trilog.norm_phi_lt_one {x : ℝ} (hx : 0 < x) : ‖phi x‖ < 1

theorem LeanPolyLog.Trilog.phi_ne_zero {x : ℝ} (hx : -1 < x) : phi x ≠ 0

theorem LeanPolyLog.Trilog.one_sub_psi (x : ℝ) : 1 - psi x = ↑(1 + x) * ((1 - Complex.I) / 2)

1 - ψ(x) = (1 + x)(1 - i)/2.

theorem LeanPolyLog.Trilog.log_one_sub_psi {x : ℝ} (hx : -1 < x) : Complex.log (1 - psi x) = ↑(Real.log (1 + x)) + Complex.log ((1 - Complex.I) / 2)

log(1 - ψ(x)) = log(1 + x) + log((1 - i)/2) for x > -1.

theorem LeanPolyLog.Trilog.psi_div_psi_sub_one {x : ℝ} (hx : -1 < x) : psi x / (psi x - 1) = phi x

ψ(x)/(ψ(x) - 1) = φ(x).

theorem LeanPolyLog.Trilog.psi_zero : psi 0 = (1 + Complex.I) / 2

theorem LeanPolyLog.Trilog.psi_one : psi 1 = Complex.I

theorem LeanPolyLog.Trilog.phi_zero : phi 0 = -Complex.I

theorem LeanPolyLog.Trilog.phi_one : phi 1 = (1 - Complex.I) / 2

Derivatives

theorem LeanPolyLog.Trilog.hasDerivAt_psi (x : ℝ) : HasDerivAt psi ((Complex.I - 1) / 2) x

theorem LeanPolyLog.Trilog.hasDerivAt_phi {x : ℝ} (hx : -1 < x) : HasDerivAt phi ((1 + Complex.I) / (↑x + 1) ^ 2) x

theorem LeanPolyLog.Trilog.deriv_psi_div_psi {x : ℝ} (hx : -1 < x) : (Complex.I - 1) / 2 / psi x = 1 / (↑x - Complex.I)

ψ'/ψ = 1/(x - i).

theorem LeanPolyLog.Trilog.deriv_phi_div_phi {x : ℝ} (hx : -1 < x) : (1 + Complex.I) / (↑x + 1) ^ 2 / phi x = 1 / (↑x - Complex.I) - 1 / (↑x + 1)

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

The primitive

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

A primitive of log²(1 + x)/(x - i) on (0, 1): with μ = log((1 - i)/2), μ² log ψ - 2 log(1 + x) Li₂(ψ) + 2 Li₃(φ) + 2 Li₃(ψ) - (log(1 + x) + μ)³/3.

Equations

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

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

On (0, 1), primM' = log²(1 + x)/(x - i).

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

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

theorem LeanPolyLog.Trilog.continuous_psi : Continuous psi

theorem LeanPolyLog.Trilog.continuousOn_phi : ContinuousOn phi (Set.Icc 0 1)

theorem LeanPolyLog.Trilog.continuousOn_primM : ContinuousOn primM (Set.Icc 0 1)

primM is continuous on [0, 1]: ψ and φ stay in the closed unit disk, where Li₂ and Li₃ are continuous, and ψ stays in the upper half-plane.

The integral

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

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

theorem LeanPolyLog.Trilog.im_primM_one_sub_primM_zero : (primM 1 - primM 0).im = 7 * Real.pi ^ 3 / 64 + 3 * Real.pi / 16 * Real.log 2 ^ 2 - 2 * G * Real.log 2 - 4 * (Li 3 ((1 + Complex.I) / 2)).im

Im (primM 1 - primM 0) = 7π³/64 + (3π/16) log² 2 - 2 G log 2 - 4 Im Li₃((1+i)/2).

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

∫₀¹ log²(1 + x)/(1 + x²) dx = 7π³/64 + (3π/16) log² 2 - 2 G log 2 - 4 Im Li₃((1+i)/2).