The integral ∫₀¹ (log³((1+r)/2) - log³((1-r)/2))/r dr

This file evaluates the real integral that the radial argument of A015 produces: ∫₀¹ (log³((1+r)/2) - log³((1-r)/2))/r dr = 2π⁴/15 + π² log² 2 - log⁴ 2/4 - 6 Li₄(1/2).

Main results

• LeanPolyLog.LogSinSq.integral_pow_mul_log_cube: ∫₀¹ tᵐ log³ t dt = -6/(m+1)⁴.
• LeanPolyLog.LogSinSq.Lir_four_one: Li₄(1) = ζ(4) = π⁴/90.
• LeanPolyLog.LogSinSq.integral_log_cube_one_sub_div: ∫₀¹ (log³((1-r)/2) + log³ 2)/r dr = -π⁴/15 - 6 log 2 ζ(3) - (π²/2) log² 2.
• LeanPolyLog.LogSinSq.integral_log_cube_one_add_div: `∫₀¹ (log³((1+r)/2) + log³ 2)/r dr = π⁴/15 - 6 log 2 ζ(3) + (π²/2) log² 2 - log⁴ 2/4
  • 6 Li₄(1/2)`.
• LeanPolyLog.LogSinSq.integral_log_cube_div: the difference of the two.

Proof sketch

Write c = log 2. Adding c³ to both cubes makes each integrand bounded near r = 0.

• The (1-r) part: with s = 1 - r it becomes ∫₀¹ φ(s)/(1-s) ds, where φ(s) = log³(s/2) + c³ = log³ s - 3c log² s + 3c² log s ≤ 0. Expanding 1/(1-s) = ∑ sⁿ and integrating term by term with the moments ∫₀¹ sⁿ logᵏ s ds = (-1)ᵏ k!/(n+1)^(k+1) gives -6ζ(4) - 6c ζ(3) - 3c² ζ(2). This value is nonzero, so the integrand is integrable.
• The (1+r) part has the explicit antiderivative (with ℓ = c - log(1+r), w = 1/(1+r)) ℓ⁴/4 - c³ℓ + log(1-w)(c³ - ℓ³) - 3ℓ² Li₂(w) + 6ℓ Li₃(w) - 6 Li₄(w), where log(1-w) (c³ - ℓ³) = (log r · log(1+r) - log²(1+r)) (ℓ² + ℓc + c²) is continuous at r = 0. It runs from -(3/4)c⁴ - 3c² ζ(2) + 6c ζ(3) - 6ζ(4) at r = 0 to -c⁴ - 6 Li₄(1/2) at r = 1. The integrand is nonnegative, so it is integrable.
• In the difference ζ(3) cancels.

The moments ∫₀¹ tᵐ log³ t dt

theorem LeanPolyLog.LogSinSq.continuousOn_mul_log_cube : ContinuousOn (fun (t : ℝ) => t * Real.log t ^ 3) (Set.Ici 0)

t log³ t is continuous on [0, ∞): with u = √(√t) it equals 64 u (u log u)³.

noncomputable def LeanPolyLog.LogSinSq.powMulLogCubePrimitive (m : ℕ) (t : ℝ) : ℝ

An antiderivative of tᵐ log³ t. It is continuous on [0, 1] and vanishes at 0.

Equations

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

theorem LeanPolyLog.LogSinSq.hasDerivAt_powMulLogCubePrimitive (m : ℕ) {t : ℝ} (ht : t ≠ 0) : HasDerivAt (powMulLogCubePrimitive m) (t ^ m * Real.log t ^ 3) t

Away from 0, the derivative of powMulLogCubePrimitive m is tᵐ log³ t.

theorem LeanPolyLog.LogSinSq.continuousOn_powMulLogCubePrimitive (m : ℕ) : ContinuousOn (powMulLogCubePrimitive m) (Set.Icc 0 1)

powMulLogCubePrimitive m is continuous on [0, 1].

theorem LeanPolyLog.LogSinSq.intervalIntegrable_pow_mul_log_cube (m : ℕ) : IntervalIntegrable (fun (t : ℝ) => t ^ m * Real.log t ^ 3) MeasureTheory.volume 0 1

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

theorem LeanPolyLog.LogSinSq.integral_pow_mul_log_cube (m : ℕ) : ∫ (t : ℝ) in 0..1, t ^ m * Real.log t ^ 3 = -(6 / (↑m + 1) ^ 4)

∫₀¹ tᵐ log³ t dt = -6/(m+1)⁴.

Zeta values

theorem LeanPolyLog.LogSinSq.hasSum_zeta_two_succ : HasSum (fun (n : ℕ) => 1 / (↑n + 1) ^ 2) (Real.pi ^ 2 / 6)

∑_{n ≥ 0} 1/(n+1)² = π²/6.

theorem LeanPolyLog.LogSinSq.hasSum_zeta_four_succ : HasSum (fun (n : ℕ) => 1 / (↑n + 1) ^ 4) (Real.pi ^ 4 / 90)

∑_{n ≥ 0} 1/(n+1)⁴ = π⁴/90.

theorem LeanPolyLog.LogSinSq.Lir_four_one : Lir 4 1 = Real.pi ^ 4 / 90

Li₄(1) = ζ(4) = π⁴/90.

theorem LeanPolyLog.LogSinSq.zeta3_nonneg : 0 ≤ zeta3

ζ(3) ≥ 0.

The (1 - r) part

noncomputable def LeanPolyLog.LogSinSq.phi (s : ℝ) : ℝ

φ(s) = log³ s - 3 log 2 · log² s + 3 log² 2 · log s, which is log³(s/2) + log³ 2 for s > 0.

Equations

• LeanPolyLog.LogSinSq.phi s = Real.log s ^ 3 - 3 * Real.log 2 * Real.log s ^ 2 + 3 * Real.log 2 ^ 2 * Real.log s

theorem LeanPolyLog.LogSinSq.intervalIntegrable_pow_mul_phi (n : ℕ) : IntervalIntegrable (fun (s : ℝ) => s ^ n * phi s) MeasureTheory.volume 0 1

sⁿ φ(s) is integrable on [0, 1].

theorem LeanPolyLog.LogSinSq.integral_pow_mul_phi (n : ℕ) : ∫ (s : ℝ) in 0..1, s ^ n * phi s = -(6 * (1 / (↑n + 1) ^ 4)) - 6 * Real.log 2 * (1 / (↑n + 1) ^ 3) - 3 * Real.log 2 ^ 2 * (1 / (↑n + 1) ^ 2)

∫₀¹ sⁿ φ(s) ds = -6/(n+1)⁴ - 6 log 2/(n+1)³ - 3 log² 2/(n+1)².

theorem LeanPolyLog.LogSinSq.phi_nonpos {s : ℝ} (hs : s ∈ Set.Icc 0 1) : phi s ≤ 0

φ ≤ 0 on [0, 1].

theorem LeanPolyLog.LogSinSq.integral_norm_pow_mul_phi (n : ℕ) : ∫ (s : ℝ) in 0..1, ‖s ^ n * phi s‖ = 6 * (1 / (↑n + 1) ^ 4) + 6 * Real.log 2 * (1 / (↑n + 1) ^ 3) + 3 * Real.log 2 ^ 2 * (1 / (↑n + 1) ^ 2)

∫₀¹ ‖sⁿ φ(s)‖ ds = 6/(n+1)⁴ + 6 log 2/(n+1)³ + 3 log² 2/(n+1)².

theorem LeanPolyLog.LogSinSq.integral_phi_div_one_sub : ∫ (s : ℝ) in 0..1, phi s / (1 - s) = -(Real.pi ^ 4 / 15) - 6 * Real.log 2 * zeta3 - Real.pi ^ 2 / 2 * Real.log 2 ^ 2

∫₀¹ φ(s)/(1-s) ds = -π⁴/15 - 6 log 2 ζ(3) - (π²/2) log² 2.

theorem LeanPolyLog.LogSinSq.integral_log_cube_one_sub_div : ∫ (r : ℝ) in 0..1, (Real.log ((1 - r) / 2) ^ 3 + Real.log 2 ^ 3) / r = -(Real.pi ^ 4 / 15) - 6 * Real.log 2 * zeta3 - Real.pi ^ 2 / 2 * Real.log 2 ^ 2

∫₀¹ (log³((1-r)/2) + log³ 2)/r dr = -π⁴/15 - 6 log 2 ζ(3) - (π²/2) log² 2.

theorem LeanPolyLog.LogSinSq.intervalIntegrable_log_cube_one_sub_div : IntervalIntegrable (fun (r : ℝ) => (Real.log ((1 - r) / 2) ^ 3 + Real.log 2 ^ 3) / r) MeasureTheory.volume 0 1

(log³((1-r)/2) + log³ 2)/r is integrable on [0, 1], since its integral is nonzero.

The (1 + r) part

noncomputable def LeanPolyLog.LogSinSq.plusPrimitive (r : ℝ) : ℝ

An antiderivative of (log³((1+r)/2) + log³ 2)/r for r > 0. With c = log 2, ℓ = c - log(1+r) and w = 1/(1+r) it is ℓ⁴/4 - c³ℓ + (log r log(1+r) - log²(1+r)) (ℓ² + ℓc + c²) - 3ℓ² Li₂(w) + 6ℓ Li₃(w) - 6 Li₄(w).

Equations

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

theorem LeanPolyLog.LogSinSq.hasDerivAt_plusPrimitive {r : ℝ} (hr0 : 0 < r) : HasDerivAt plusPrimitive ((Real.log ((1 + r) / 2) ^ 3 + Real.log 2 ^ 3) / r) r

For r > 0, plusPrimitive' r = (log³((1+r)/2) + log³ 2)/r.

theorem LeanPolyLog.LogSinSq.continuousOn_plusPrimitive : ContinuousOn plusPrimitive (Set.Icc 0 1)

plusPrimitive is continuous on [0, 1].

theorem LeanPolyLog.LogSinSq.log_cube_one_add_div_nonneg {r : ℝ} (hr : 0 < r) : 0 ≤ (Real.log ((1 + r) / 2) ^ 3 + Real.log 2 ^ 3) / r

(log³((1+r)/2) + log³ 2)/r ≥ 0 for r > 0.

theorem LeanPolyLog.LogSinSq.intervalIntegrable_log_cube_one_add_div : IntervalIntegrable (fun (r : ℝ) => (Real.log ((1 + r) / 2) ^ 3 + Real.log 2 ^ 3) / r) MeasureTheory.volume 0 1

(log³((1+r)/2) + log³ 2)/r is integrable on [0, 1].

theorem LeanPolyLog.LogSinSq.integral_log_cube_one_add_div : ∫ (r : ℝ) in 0..1, (Real.log ((1 + r) / 2) ^ 3 + Real.log 2 ^ 3) / r = Real.pi ^ 4 / 15 - 6 * Real.log 2 * zeta3 + Real.pi ^ 2 / 2 * Real.log 2 ^ 2 - Real.log 2 ^ 4 / 4 - 6 * Lir 4 (1 / 2)

∫₀¹ (log³((1+r)/2) + log³ 2)/r dr = π⁴/15 - 6 log 2 ζ(3) + (π²/2) log² 2 - log⁴ 2/4 - 6 Li₄(1/2).

The difference

theorem LeanPolyLog.LogSinSq.intervalIntegrable_log_cube_div : IntervalIntegrable (fun (r : ℝ) => (Real.log ((1 + r) / 2) ^ 3 - Real.log ((1 - r) / 2) ^ 3) / r) MeasureTheory.volume 0 1

The integrand of the radial argument is integrable on [0, 1].

theorem LeanPolyLog.LogSinSq.integral_log_cube_div : ∫ (r : ℝ) in 0..1, (Real.log ((1 + r) / 2) ^ 3 - Real.log ((1 - r) / 2) ^ 3) / r = 2 * Real.pi ^ 4 / 15 + Real.pi ^ 2 * Real.log 2 ^ 2 - Real.log 2 ^ 4 / 4 - 6 * Lir 4 (1 / 2)

∫₀¹ (log³((1+r)/2) - log³((1-r)/2))/r dr = 2π⁴/15 + π² log² 2 - log⁴ 2/4 - 6 Li₄(1/2).