The trilogarithm, log² moments and a symmetric double integral

This file collects the lemmas behind A013, one power of log higher than LeanPool.PolylogIntegrals.Lemmas.Arctan.

Main results

• LeanPolyLog.Arctan.integral_pow_mul_log_sq: ∫₀¹ tᵐ log² t dt = 2/(m+1)³.
• LeanPolyLog.Arctan.integral_mul_log_sq_div_one_add_mul: for 0 ≤ x ≤ 1, ∫₀¹ x log² y/(1 + xy) dy = -2 Li₃(-x).
• LeanPolyLog.Arctan.Lir_three_one, LeanPolyLog.Arctan.Lir_three_neg_one: Li₃(1) = ζ(3) and Li₃(-1) = -(3/4) ζ(3).
• LeanPolyLog.Arctan.hasSum_eta_three, LeanPolyLog.Arctan.hasSum_beta_three: η(3) = ∑ (-1)ⁿ/(n+1)³ = (3/4) ζ(3) and β(3) = ∑ (-1)ᵏ/(2k+1)³ = π³/32.
• LeanPolyLog.Arctan.integral_log_sq_div_one_add_sq, LeanPolyLog.Arctan.integral_mul_log_sq_div_one_add_sq: ∫₀¹ log² y/(1+y²) dy = π³/16 and ∫₀¹ y log² y/(1+y²) dy = (3/16) ζ(3).
• LeanPolyLog.Arctan.integral_log_mul_Lir_two_neg_div_one_add_sq: ∫₀¹ log x · Li₂(-x)/(1+x²) dx = π² G/48.
• LeanPolyLog.Arctan.hasDerivAt_trilog_primitive: on (0, 1), -2 Li₃(-x) + 2 log x · Li₂(-x) + log(1+x) log² x is an antiderivative of log² x/(1+x); it is continuous on [0, 1] by LeanPolyLog.Arctan.continuousOn_log_mul_Lir_two_neg and LeanPolyLog.Arctan.continuousOn_log_one_add_mul_log_sq.

Proof sketch

• The log² moments come from the antiderivative t^(m+1) (log² t/(m+1) - 2 log t/(m+1)² + 2/(m+1)³), which is continuous at 0 because t log² t = 4 (√t log √t)² for t ≥ 0.
• Li₃(-1) follows from the duplication formula Li₃(1) = 4 (Li₃(1) + Li₃(-1)), and β(3) is Mathlib's hasSum_L_function_mod_four_eval_three, restricted to the odd indices.
• For the double integral, write Li₂(-x) = ∫₀¹ x log y/(1+xy) dy. The integrand f(x, y) = x log x log y/((1+x²)(1+xy)) is bounded by |log x| |log y| on (0, 1]², and f(x, y) + f(y, x) = (x log x/(1+x²)) (log y/(1+y²)) + (log x/(1+x²)) (y log y/(1+y²)). Swapping the variables gives twice the integral as a sum of two products of single integrals, 2 (-π²/48)(-G).
• Continuity at 0: log x · Li₂(-x) = -(x log x) ∑ (-x)ⁿ/(n+1)², and 0 ≤ log(1+x) log² x ≤ x log² x on [0, 1].

The moments ∫₀¹ tᵐ log² t dt

theorem LeanPolyLog.Arctan.continuousOn_mul_log_sq : ContinuousOn (fun (t : ℝ) => t * Real.log t ^ 2) (Set.Ici 0)

t log² t is continuous on [0, ∞): there it equals 4 (√t log √t)².

noncomputable def LeanPolyLog.Arctan.powMulLogSqPrimitive (m : ℕ) (t : ℝ) : ℝ

An antiderivative of tᵐ log² t, namely t^(m+1) log² t/(m+1) - 2 t^(m+1) log t/(m+1)² + 2 t^(m+1)/(m+1)³. It is continuous on [0, 1] and vanishes at 0.

Equations

• LeanPolyLog.Arctan.powMulLogSqPrimitive m t = t ^ (m + 1) * Real.log t ^ 2 / (↑m + 1) - 2 * (t ^ (m + 1) * Real.log t) / (↑m + 1) ^ 2 + 2 * t ^ (m + 1) / (↑m + 1) ^ 3

theorem LeanPolyLog.Arctan.hasDerivAt_powMulLogSqPrimitive (m : ℕ) {t : ℝ} (ht : t ≠ 0) : HasDerivAt (powMulLogSqPrimitive m) (t ^ m * Real.log t ^ 2) t

Away from 0, the derivative of powMulLogSqPrimitive m is tᵐ log² t.

theorem LeanPolyLog.Arctan.continuousOn_powMulLogSqPrimitive (m : ℕ) : ContinuousOn (powMulLogSqPrimitive m) (Set.Icc 0 1)

powMulLogSqPrimitive m is continuous on [0, 1].

theorem LeanPolyLog.Arctan.intervalIntegrable_pow_mul_log_sq (m : ℕ) : IntervalIntegrable (fun (t : ℝ) => t ^ m * Real.log t ^ 2) MeasureTheory.volume 0 1

tᵐ log² t is integrable on [0, 1]: it is the nonnegative derivative of a continuous function.

theorem LeanPolyLog.Arctan.integral_pow_mul_log_sq (m : ℕ) : ∫ (t : ℝ) in 0..1, t ^ m * Real.log t ^ 2 = 2 / (↑m + 1) ^ 3

∫₀¹ tᵐ log² t dt = 2/(m+1)³.

theorem LeanPolyLog.Arctan.integral_norm_pow_mul_log_sq (m : ℕ) : ∫ (t : ℝ) in 0..1, ‖t ^ m * Real.log t ^ 2‖ = 2 / (↑m + 1) ^ 3

∫₀¹ ‖tᵐ log² t‖ dt = 2/(m+1)³.

The trilogarithm as an integral

theorem LeanPolyLog.Arctan.integral_mul_log_sq_div_one_add_mul {x : ℝ} (hx0 : 0 ≤ x) (hx1 : x ≤ 1) : ∫ (y : ℝ) in 0..1, x * Real.log y ^ 2 / (1 + x * y) = -2 * Lir 3 (-x)

For 0 ≤ x ≤ 1: ∫₀¹ x log² y/(1 + xy) dy = -2 Li₃(-x).

ζ(3)-type values

theorem LeanPolyLog.Arctan.Lir_three_one : Lir 3 1 = zeta3

Li₃(1) = ζ(3).

theorem LeanPolyLog.Arctan.Lir_three_neg_one : Lir 3 (-1) = -(3 / 4 * zeta3)

Li₃(-1) = -η(3) = -(3/4) ζ(3), from the duplication formula at x = 1.

theorem LeanPolyLog.Arctan.hasSum_eta_three : HasSum (fun (n : ℕ) => (-1) ^ n / (↑n + 1) ^ 3) (3 / 4 * zeta3)

The Dirichlet eta function at 3: η(3) = ∑_{n ≥ 0} (-1)ⁿ/(n+1)³ = (3/4) ζ(3).

theorem LeanPolyLog.Arctan.hasSum_beta_three : HasSum (fun (k : ℕ) => (-1) ^ k / (2 * ↑k + 1) ^ 3) (Real.pi ^ 3 / 32)

The Dirichlet beta function at 3: β(3) = ∑_{k ≥ 0} (-1)ᵏ/(2k+1)³ = π³/32.

Two more integrals against 1/(1+y²)

theorem LeanPolyLog.Arctan.integral_log_sq_div_one_add_sq : ∫ (y : ℝ) in 0..1, Real.log y ^ 2 / (1 + y ^ 2) = Real.pi ^ 3 / 16

∫₀¹ log² y/(1+y²) dy = 2 β(3) = π³/16.

theorem LeanPolyLog.Arctan.integral_mul_log_sq_div_one_add_sq : ∫ (y : ℝ) in 0..1, y * Real.log y ^ 2 / (1 + y ^ 2) = 3 / 16 * zeta3

∫₀¹ y log² y/(1+y²) dy = η(3)/4 = (3/16) ζ(3).

The symmetric double integral

theorem LeanPolyLog.Arctan.integral_log_mul_Lir_two_neg_div_one_add_sq : ∫ (x : ℝ) in 0..1, Real.log x * Lir 2 (-x) / (1 + x ^ 2) = Real.pi ^ 2 * G / 48

∫₀¹ log x · Li₂(-x)/(1+x²) dx = π² G/48.

With Li₂(-x) = ∫₀¹ x log y/(1+xy) dy this is the integral of f(x, y) = x log x log y/((1+x²)(1+xy)) over the square, which equals that of f(y, x); and f(x, y) + f(y, x) = (x log x/(1+x²)) (log y/(1+y²)) + (log x/(1+x²)) (y log y/(1+y²)).

Continuity of the pieces of the antiderivative at 0

theorem LeanPolyLog.Arctan.continuousOn_tsum_neg_pow_div_sq : ContinuousOn (fun (x : ℝ) => ∑' (n : ℕ), (-x) ^ n / (↑n + 1) ^ 2) (Set.Icc 0 1)

x ↦ ∑ (-x)ⁿ/(n+1)² is continuous on [0, 1] (Weierstrass M-test).

theorem LeanPolyLog.Arctan.Lir_two_neg_eq (x : ℝ) : Lir 2 (-x) = -x * ∑' (n : ℕ), (-x) ^ n / (↑n + 1) ^ 2

Li₂(-x) = -x ∑ (-x)ⁿ/(n+1)².

theorem LeanPolyLog.Arctan.continuousOn_log_mul_Lir_two_neg : ContinuousOn (fun (x : ℝ) => Real.log x * Lir 2 (-x)) (Set.Icc 0 1)

x ↦ log x · Li₂(-x) is continuous on [0, 1]: it equals -(x log x) ∑ (-x)ⁿ/(n+1)².

theorem LeanPolyLog.Arctan.continuousOn_log_one_add_mul_log_sq : ContinuousOn (fun (x : ℝ) => Real.log (1 + x) * Real.log x ^ 2) (Set.Icc 0 1)

x ↦ log(1+x) log² x is continuous on [0, 1]: at 0 it is squeezed between 0 and x log² x.

An antiderivative of log² x/(1+x)

theorem LeanPolyLog.Arctan.hasDerivAt_trilog_primitive {x : ℝ} (hx0 : 0 < x) (hx1 : x < 1) : HasDerivAt (fun (x : ℝ) => -2 * Lir 3 (-x) + 2 * (Real.log x * Lir 2 (-x)) + Real.log (1 + x) * Real.log x ^ 2) (Real.log x ^ 2 / (1 + x)) x

On (0, 1), d/dx [-2 Li₃(-x) + 2 log x · Li₂(-x) + log(1+x) log² x] = log² x/(1+x).