Integrals against 1/(1+x²) and the kernel of A012

This file collects the lemmas behind A012 (and A013): termwise integration of geometric series over [0, 1], the integral representation of Li₂(-x), an explicit kernel, and the Fubini swap that connects them.

Main results

• LeanPolyLog.Arctan.hasSum_integral_div_one_sub: termwise integration of φ(y)/(1 - q(y)) = ∑ q(y)ⁿ φ(y) over [0, 1], when |q| < 1 on (0, 1) and the integrals of the norms of the terms are summable.
• LeanPolyLog.Arctan.hasSum_integral_mul_div_one_add_mul, LeanPolyLog.Arctan.hasSum_integral_div_one_add_sq: the cases q(y) = -xy and q(y) = -y².
• LeanPolyLog.Arctan.integral_pow_mul_log: ∫₀¹ tᵐ log t dt = -1/(m+1)².
• LeanPolyLog.Arctan.integral_mul_log_div_one_add_mul: for 0 ≤ x ≤ 1, ∫₀¹ x log y/(1 + xy) dy = Li₂(-x).
• LeanPolyLog.Arctan.integral_kernel: for y ≥ 0, ∫₀¹ x/((1+x²)(1+xy)) dx = (log 2/2 + πy/4 - log(1+y))/(1+y²).
• LeanPolyLog.Arctan.integral_integral_swap_kernel: for φ integrable on [0, 1], ∫₀¹ (1+x²)⁻¹ ∫₀¹ x φ(y)/(1+xy) dy dx = ∫₀¹ φ(y) ∫₀¹ x/((1+x²)(1+xy)) dx dy.
• LeanPolyLog.Arctan.integral_log_div_one_add_sq, LeanPolyLog.Arctan.integral_mul_log_div_one_add_sq: ∫₀¹ log y/(1+y²) dy = -G and ∫₀¹ y log y/(1+y²) dy = -π²/48.
• LeanPolyLog.Arctan.hasDerivAt_Lir_two_neg_add: on (0, 1), Li₂(-x) + log x · log(1+x) is an antiderivative of log x/(1+x).

Proof sketch

• Termwise integration is MeasureTheory.hasSum_integral_of_summable_integral_norm. The geometric series ∑ q(y)ⁿ converges on (0, 1), which differs from (0, 1] by a null set.
• For Li₂(-x), expand x log y/(1+xy) = ∑ (-x)ⁿ x yⁿ log y and use ∫₀¹ yⁿ log y dy = -1/(n+1)²; the norms of the terms integrate to x^(n+1)/(n+1)².
• The kernel has the explicit antiderivative (log(1+x²)/2 + y arctan x - log(1+xy))/(1+y²) (partial fractions).
• For the swap, on (0, 1]² the integrand x φ(y)/((1+x²)(1+xy)) is bounded by |φ(y)|, which is integrable on the square, so Fubini applies (intervalIntegral_intervalIntegral_swap).
• ∫₀¹ y log y/(1+y²) dy = ∑ (-1)ⁿ ∫₀¹ y^(2n+1) log y dy = -η(2)/4 = -π²/48.

Termwise integration of geometric series

theorem LeanPolyLog.Arctan.hasSum_integral_div_one_sub {φ q : ℝ → ℝ} (hq : ∀ y ∈ Set.Ioo 0 1, |q y| < 1) (hint : ∀ (n : ℕ), IntervalIntegrable (fun (y : ℝ) => q y ^ n * φ y) MeasureTheory.volume 0 1) (hsum : Summable fun (n : ℕ) => ∫ (y : ℝ) in 0..1, ‖q y ^ n * φ y‖) : HasSum (fun (n : ℕ) => ∫ (y : ℝ) in 0..1, q y ^ n * φ y) (∫ (y : ℝ) in 0..1, φ y / (1 - q y))

Termwise integration of φ(y)/(1 - q(y)) = ∑ q(y)ⁿ φ(y) over [0, 1], when |q(y)| < 1 on (0, 1) and the integrals of the norms of the terms are summable.

theorem LeanPolyLog.Arctan.hasSum_integral_mul_div_one_add_mul {ψ : ℝ → ℝ} {x : ℝ} (hx0 : 0 ≤ x) (hx1 : x ≤ 1) (hint : ∀ (n : ℕ), IntervalIntegrable (fun (y : ℝ) => y ^ n * ψ y) MeasureTheory.volume 0 1) (hsum : Summable fun (n : ℕ) => ∫ (y : ℝ) in 0..1, ‖y ^ n * ψ y‖) : HasSum (fun (n : ℕ) => (-x) ^ n * x * ∫ (y : ℝ) in 0..1, y ^ n * ψ y) (∫ (y : ℝ) in 0..1, x * ψ y / (1 + x * y))

For 0 ≤ x ≤ 1: ∫₀¹ x ψ(y)/(1 + xy) dy = ∑ (-x)ⁿ x ∫₀¹ yⁿ ψ(y) dy, provided the moments ∫₀¹ ‖yⁿ ψ(y)‖ dy are summable.

theorem LeanPolyLog.Arctan.hasSum_integral_div_one_add_sq {ψ : ℝ → ℝ} (hint : ∀ (n : ℕ), IntervalIntegrable (fun (y : ℝ) => y ^ (2 * n) * ψ y) MeasureTheory.volume 0 1) (hsum : Summable fun (n : ℕ) => ∫ (y : ℝ) in 0..1, ‖y ^ (2 * n) * ψ y‖) : HasSum (fun (n : ℕ) => (-1) ^ n * ∫ (y : ℝ) in 0..1, y ^ (2 * n) * ψ y) (∫ (y : ℝ) in 0..1, ψ y / (1 + y ^ 2))

∫₀¹ ψ(y)/(1 + y²) dy = ∑ (-1)ⁿ ∫₀¹ y²ⁿ ψ(y) dy, provided the moments ∫₀¹ ‖y²ⁿ ψ(y)‖ dy are summable.

The moments ∫₀¹ tᵐ log t dt

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

tᵐ log t is integrable on [0, 1].

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

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

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

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

The dilogarithm as an integral

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

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

The kernel ∫₀¹ x/((1+x²)(1+xy)) dx and the Fubini swap

theorem LeanPolyLog.Arctan.continuous_inv_one_add_sq : Continuous fun (x : ℝ) => (1 + x ^ 2)⁻¹

x ↦ (1 + x²)⁻¹ is continuous.

theorem LeanPolyLog.Arctan.integral_kernel {y : ℝ} (hy : 0 ≤ y) : ∫ (x : ℝ) in 0..1, x / ((1 + x ^ 2) * (1 + x * y)) = (Real.log 2 / 2 + Real.pi / 4 * y - Real.log (1 + y)) / (1 + y ^ 2)

For y ≥ 0: ∫₀¹ x/((1+x²)(1+xy)) dx = (log 2/2 + πy/4 - log(1+y))/(1+y²).

theorem LeanPolyLog.Arctan.integral_integral_swap_kernel {φ : ℝ → ℝ} (hφ : IntervalIntegrable φ MeasureTheory.volume 0 1) : ∫ (x : ℝ) in 0..1, (1 + x ^ 2)⁻¹ * ∫ (y : ℝ) in 0..1, x * φ y / (1 + x * y) = ∫ (y : ℝ) in 0..1, φ y * ∫ (x : ℝ) in 0..1, x / ((1 + x ^ 2) * (1 + x * y))

Fubini for the kernel: for φ integrable on [0, 1], ∫₀¹ (1+x²)⁻¹ ∫₀¹ x φ(y)/(1+xy) dy dx = ∫₀¹ φ(y) ∫₀¹ x/((1+x²)(1+xy)) dx dy.

Two integrals against 1/(1+y²)

theorem LeanPolyLog.Arctan.integral_log_div_one_add_sq : ∫ (y : ℝ) in 0..1, Real.log y / (1 + y ^ 2) = -G

∫₀¹ log y/(1+y²) dy = -G.

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

∫₀¹ y log y/(1+y²) dy = -η(2)/4 = -π²/48.

An antiderivative of log x/(1+x)

theorem LeanPolyLog.Arctan.continuous_log_mul_log_one_add : Continuous fun (x : ℝ) => Real.log x * Real.log (1 + x)

x ↦ log x · log(1+x) is continuous on ℝ (with Lean's log 0 = 0).

theorem LeanPolyLog.Arctan.continuousOn_Lir_neg {s : ℕ} (hs : 2 ≤ s) : ContinuousOn (fun (x : ℝ) => Lir s (-x)) (Set.Icc 0 1)

For s ≥ 2, x ↦ Li_s(-x) is continuous on [0, 1].

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

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