Polylogarithms against the arcsine weight

This file proves the identity behind A011 and A016. Let s ≥ 2, and let w ≥ 0 on (0, 1] have the moments ∫₀¹ yⁿ w(y) dy = 1/(n+1)^s. Then ∫₀¹ Li_s(x) / (x √(1 - x²)) dx = ∫₀^{π/2} w(sin φ) (π/2 + φ) dφ. The weight w = -log (with s = 2) gives A011, and w = log²/2 (with s = 3) gives A016.

Main results

• LeanPolyLog.Arcsin.hasDerivAt_arcsin_div: for |x|, |y| < 1, d/dx arcsin ((x - y)/(1 - xy)) = √(1 - y²) / ((1 - xy) √(1 - x²)).
• LeanPolyLog.Arcsin.integral_one_div_mul_sqrt: for |y| < 1, ∫₀¹ dx / ((1 - xy) √(1 - x²)) = (π/2 + arcsin y) / √(1 - y²).
• LeanPolyLog.Arcsin.integral_div_one_sub_mul: for 0 < x < 1, ∫₀¹ w(y) / (1 - xy) dy = Li_s(x)/x.
• LeanPolyLog.Arcsin.integral_Lir_div_mul_sqrt_eq_integral_arcsin: ∫₀¹ Li_s(x) / (x √(1 - x²)) dx = ∫₀¹ w(y) (π/2 + arcsin y) / √(1 - y²) dy.
• LeanPolyLog.Arcsin.integral_mul_arcsin_div_sqrt: the substitution y = sin φ, for any w.
• LeanPolyLog.Arcsin.integral_Lir_div_mul_sqrt: ∫₀¹ Li_s(x) / (x √(1 - x²)) dx = ∫₀^{π/2} w(sin φ) (π/2 + φ) dφ.

Proof sketch

• Li_s(x)/x = ∑ xⁿ/(n+1)^s = ∑ xⁿ ∫₀¹ yⁿ w(y) dy = ∫₀¹ w(y)/(1 - xy) dy. The termwise integration is justified because the terms are nonnegative and their integrals are summable.
• So the integral is ∫₀¹ ∫₀¹ w(y) / ((1 - xy) √(1 - x²)) dy dx. The integrand is nonnegative and integrable on the square: for fixed x it is at most a multiple of w(y), and its integral in y is Li_s(x) / (x √(1 - x²)) ≤ Li_s(1) / √(1 - x²). Fubini swaps the two integrals.
• The integral in x is elementary: arcsin ((x - y)/(1 - xy)) is an antiderivative of √(1 - y²) / ((1 - xy) √(1 - x²)), and it runs from -arcsin y at x = 0 to π/2 at x = 1.
• Finally y = sin φ turns dy / √(1 - y²) into dφ and arcsin y into φ.

In Lean √0 = 0 and a / 0 = 0, so the integrands are 0 at x = 1 or y = 1. Single points do not affect the integrals, and the proofs work on the open square (0, 1)².

The kernel 1/((1 - xy) √(1 - x²))

theorem LeanPolyLog.Arcsin.one_sub_mul_pos {x y : ℝ} (hx : x ∈ Set.Icc 0 1) (hy : y ∈ Set.Ioo (-1) 1) : 0 < 1 - x * y

1 - xy > 0 for x ∈ [0, 1] and |y| < 1.

theorem LeanPolyLog.Arcsin.one_sub_sq_div_one_sub_mul {x y : ℝ} (h : 1 - x * y ≠ 0) : 1 - ((x - y) / (1 - x * y)) ^ 2 = (1 - x ^ 2) * (1 - y ^ 2) / (1 - x * y) ^ 2

1 - ((x - y)/(1 - xy))² = (1 - x²)(1 - y²)/(1 - xy)².

theorem LeanPolyLog.Arcsin.hasDerivAt_arcsin_div {x y : ℝ} (hx : x ∈ Set.Ioo (-1) 1) (hy : y ∈ Set.Ioo (-1) 1) : HasDerivAt (fun (x : ℝ) => Real.arcsin ((x - y) / (1 - x * y))) (√(1 - y ^ 2) / ((1 - x * y) * √(1 - x ^ 2))) x

For |x|, |y| < 1: d/dx arcsin ((x - y)/(1 - xy)) = √(1 - y²) / ((1 - xy) √(1 - x²)).

theorem LeanPolyLog.Arcsin.continuousOn_arcsin_div {y : ℝ} (hy : y ∈ Set.Ioo (-1) 1) : ContinuousOn (fun (x : ℝ) => Real.arcsin ((x - y) / (1 - x * y))) (Set.Icc 0 1)

x ↦ arcsin ((x - y)/(1 - xy)) is continuous on [0, 1] for |y| < 1.

theorem LeanPolyLog.Arcsin.sqrt_div_mul_sqrt_nonneg {x y : ℝ} (hx : x ∈ Set.Ioo 0 1) (hy : y ∈ Set.Ioo (-1) 1) : 0 ≤ √(1 - y ^ 2) / ((1 - x * y) * √(1 - x ^ 2))

The derivative in hasDerivAt_arcsin_div is nonnegative for 0 < x < 1.

theorem LeanPolyLog.Arcsin.integral_sqrt_div_mul_sqrt {y : ℝ} (hy : y ∈ Set.Ioo (-1) 1) : ∫ (x : ℝ) in 0..1, √(1 - y ^ 2) / ((1 - x * y) * √(1 - x ^ 2)) = Real.pi / 2 + Real.arcsin y

∫₀¹ √(1 - y²) / ((1 - xy) √(1 - x²)) dx = π/2 + arcsin y for |y| < 1.

theorem LeanPolyLog.Arcsin.integrableOn_one_div_mul_sqrt {y : ℝ} (hy : y ∈ Set.Ioo (-1) 1) : MeasureTheory.IntegrableOn (fun (x : ℝ) => 1 / ((1 - x * y) * √(1 - x ^ 2))) (Set.Ioc 0 1) MeasureTheory.volume

The kernel 1/((1 - xy) √(1 - x²)) is integrable on (0, 1] for |y| < 1.

theorem LeanPolyLog.Arcsin.integrableOn_one_div_sqrt : MeasureTheory.IntegrableOn (fun (x : ℝ) => 1 / √(1 - x ^ 2)) (Set.Ioc 0 1) MeasureTheory.volume

1/√(1 - x²) is integrable on (0, 1].

theorem LeanPolyLog.Arcsin.integral_one_div_mul_sqrt {y : ℝ} (hy : y ∈ Set.Ioo (-1) 1) : ∫ (x : ℝ) in 0..1, 1 / ((1 - x * y) * √(1 - x ^ 2)) = (Real.pi / 2 + Real.arcsin y) / √(1 - y ^ 2)

∫₀¹ dx / ((1 - xy) √(1 - x²)) = (π/2 + arcsin y) / √(1 - y²) for |y| < 1.

Generating functions of moments

theorem LeanPolyLog.Arcsin.hasSum_Lir_div_self {s : ℕ} (hs : 2 ≤ s) {x : ℝ} (hx : |x| ≤ 1) (hx0 : x ≠ 0) : HasSum (fun (n : ℕ) => x ^ n / (↑n + 1) ^ s) (Lir s x / x)

For 0 < |x| ≤ 1 and s ≥ 2: ∑_{n ≥ 0} xⁿ/(n+1)^s = Li_s(x)/x.

theorem LeanPolyLog.Arcsin.Lir_div_self_nonneg {s : ℕ} (hs : 2 ≤ s) {x : ℝ} (hx : x ∈ Set.Ioc 0 1) : 0 ≤ Lir s x / x

For 0 < x ≤ 1 and s ≥ 2: 0 ≤ Li_s(x)/x.

theorem LeanPolyLog.Arcsin.Lir_div_self_le {s : ℕ} (hs : 2 ≤ s) {x : ℝ} (hx : x ∈ Set.Ioc 0 1) : Lir s x / x ≤ Lir s 1

For 0 < x ≤ 1 and s ≥ 2: Li_s(x)/x ≤ Li_s(1).

theorem LeanPolyLog.Arcsin.integral_div_one_sub_mul {s : ℕ} {w : ℝ → ℝ} (hw0 : ∀ y ∈ Set.Ioc 0 1, 0 ≤ w y) (hint : ∀ (n : ℕ), MeasureTheory.IntegrableOn (fun (y : ℝ) => y ^ n * w y) (Set.Ioc 0 1) MeasureTheory.volume) (hmom : ∀ (n : ℕ), ∫ (y : ℝ) in 0..1, y ^ n * w y = 1 / (↑n + 1) ^ s) {x : ℝ} (hx : x ∈ Set.Ioo 0 1) : ∫ (y : ℝ) in Set.Ioc 0 1, w y / (1 - x * y) = Lir s x / x

Let w ≥ 0 on (0, 1] have the moments ∫₀¹ yⁿ w(y) dy = 1/(n+1)^s. Then for 0 < x < 1, ∫₀¹ w(y)/(1 - xy) dy = Li_s(x)/x: expand 1/(1 - xy) as a geometric series and integrate term by term.

Swapping the order of integration

theorem LeanPolyLog.Arcsin.integral_Lir_div_mul_sqrt_eq_integral_arcsin {s : ℕ} (hs : 2 ≤ s) {w : ℝ → ℝ} (hw : Measurable w) (hw0 : ∀ y ∈ Set.Ioc 0 1, 0 ≤ w y) (hint : ∀ (n : ℕ), MeasureTheory.IntegrableOn (fun (y : ℝ) => y ^ n * w y) (Set.Ioc 0 1) MeasureTheory.volume) (hmom : ∀ (n : ℕ), ∫ (y : ℝ) in 0..1, y ^ n * w y = 1 / (↑n + 1) ^ s) : ∫ (x : ℝ) in 0..1, Lir s x / (x * √(1 - x ^ 2)) = ∫ (y : ℝ) in 0..1, w y * ((Real.pi / 2 + Real.arcsin y) / √(1 - y ^ 2))

Let s ≥ 2, and let w ≥ 0 on (0, 1] be measurable with the moments ∫₀¹ yⁿ w(y) dy = 1/(n+1)^s. Then ∫₀¹ Li_s(x) / (x √(1 - x²)) dx = ∫₀¹ w(y) (π/2 + arcsin y) / √(1 - y²) dy. Both sides equal ∫₀¹ ∫₀¹ w(y) / ((1 - xy) √(1 - x²)) dx dy, by Fubini.

The substitution y = sin φ

theorem LeanPolyLog.Arcsin.integral_mul_arcsin_div_sqrt (w : ℝ → ℝ) : ∫ (y : ℝ) in 0..1, w y * ((Real.pi / 2 + Real.arcsin y) / √(1 - y ^ 2)) = ∫ (φ : ℝ) in 0..Real.pi / 2, w (Real.sin φ) * (Real.pi / 2 + φ)

The substitution y = sin φ: ∫₀¹ w(y) (π/2 + arcsin y) / √(1 - y²) dy = ∫₀^{π/2} w(sin φ) (π/2 + φ) dφ for any w.

theorem LeanPolyLog.Arcsin.integral_Lir_div_mul_sqrt {s : ℕ} (hs : 2 ≤ s) {w : ℝ → ℝ} (hw : Measurable w) (hw0 : ∀ y ∈ Set.Ioc 0 1, 0 ≤ w y) (hint : ∀ (n : ℕ), MeasureTheory.IntegrableOn (fun (y : ℝ) => y ^ n * w y) (Set.Ioc 0 1) MeasureTheory.volume) (hmom : ∀ (n : ℕ), ∫ (y : ℝ) in 0..1, y ^ n * w y = 1 / (↑n + 1) ^ s) : ∫ (x : ℝ) in 0..1, Lir s x / (x * √(1 - x ^ 2)) = ∫ (φ : ℝ) in 0..Real.pi / 2, w (Real.sin φ) * (Real.pi / 2 + φ)

Let s ≥ 2, and let w ≥ 0 on (0, 1] be measurable with the moments ∫₀¹ yⁿ w(y) dy = 1/(n+1)^s. Then ∫₀¹ Li_s(x) / (x √(1 - x²)) dx = ∫₀^{π/2} w(sin φ) (π/2 + φ) dφ.