The integral ∫₀^{π/2} log² sin x dx

This file proves ∫₀^{π/2} log² sin x dx = π³/24 + (π/2) log² 2, which A015 and A016 use.

Main results

• LeanPolyLog.LogSinSq.intervalIntegrable_log_sin_sq, LeanPolyLog.LogSinSq.intervalIntegrable_log_cos_sq, LeanPolyLog.LogSinSq.intervalIntegrable_log_sin_sq_zero_pi: log² sin is integrable on [0, π/2] and on [0, π], and log² cos is integrable on [0, π/2].
• LeanPolyLog.LogSinSq.integral_log_cos_sq: ∫₀^{π/2} log² cos = ∫₀^{π/2} log² sin.
• LeanPolyLog.LogSinSq.integral_log_sin_sq_zero_pi: ∫₀^π log² sin = 2 ∫₀^{π/2} log² sin.
• LeanPolyLog.LogSinSq.integral_log_tan_sq: ∫₀^{π/4} (log sin x - log cos x)² dx = π³/16.
• LeanPolyLog.LogSinSq.integral_log_sin_sq: ∫₀^{π/2} log² sin x dx = π³/24 + (π/2) log² 2.
• LeanPolyLog.LogSinSq.integral_log_sin_mul_log_cos: ∫₀^{π/2} log sin x · log cos x dx = (π/2) log² 2 - π³/48.

Proof sketch

Write L = ∫₀^{π/2} log² sin and B = ∫₀^{π/2} log sin · log cos; also ∫₀^{π/2} log² cos = L and ∫₀^{π/2} log cos = ∫₀^{π/2} log sin = -(π/2) log 2.

• Integrability: Jordan's inequality (2/π) x ≤ sin x ≤ 1 gives log² sin x ≤ log² (2x/π) on (0, π/2], and log² is integrable on [0, 1]. The product log sin · log cos is bounded by log² sin + log² cos.
• sin 2x = 2 sin x cos x, and u = 2x together with sin (π - u) = sin u gives ∫₀^{π/2} log² sin 2x dx = L. Expanding the square, L = 2L - (3π/2) log² 2 + 2B.
• On [0, π/4] the substitution x = arctan t turns log sin x - log cos x into log t, so ∫₀^{π/4} (log sin - log cos)² = ∫₀¹ log² t/(1+t²) dt = π³/16. The reflection x ↦ π/2 - x doubles this to ∫₀^{π/2} (log sin - log cos)² = 2L - 2B = π³/8.
• Solving the two linear equations gives L and B.

Integrability

theorem LeanPolyLog.LogSinSq.log_sin_sq_le {x : ℝ} (hx : x ∈ Set.Ioc 0 (Real.pi / 2)) : Real.log (Real.sin x) ^ 2 ≤ Real.log (2 / Real.pi * x) ^ 2

On (0, π/2], Jordan's inequality gives log² sin x ≤ log² (2x/π).

theorem LeanPolyLog.LogSinSq.intervalIntegrable_log_sq_mul : IntervalIntegrable (fun (x : ℝ) => Real.log (2 / Real.pi * x) ^ 2) MeasureTheory.volume 0 (Real.pi / 2)

log² (2x/π) is integrable on [0, π/2].

theorem LeanPolyLog.LogSinSq.intervalIntegrable_log_sin_sq : IntervalIntegrable (fun (x : ℝ) => Real.log (Real.sin x) ^ 2) MeasureTheory.volume 0 (Real.pi / 2)

log² sin is integrable on [0, π/2].

theorem LeanPolyLog.LogSinSq.intervalIntegrable_log_cos_sq : IntervalIntegrable (fun (x : ℝ) => Real.log (Real.cos x) ^ 2) MeasureTheory.volume 0 (Real.pi / 2)

log² cos is integrable on [0, π/2].

theorem LeanPolyLog.LogSinSq.intervalIntegrable_log_sin_sq_zero_pi : IntervalIntegrable (fun (x : ℝ) => Real.log (Real.sin x) ^ 2) MeasureTheory.volume 0 Real.pi

log² sin is integrable on [0, π].

theorem LeanPolyLog.LogSinSq.intervalIntegrable_log_sin_mul_log_cos : IntervalIntegrable (fun (x : ℝ) => Real.log (Real.sin x) * Real.log (Real.cos x)) MeasureTheory.volume 0 (Real.pi / 2)

log sin · log cos is integrable on [0, π/2]: it is bounded by log² sin + log² cos.

Symmetries

theorem LeanPolyLog.LogSinSq.integral_log_cos_sq : ∫ (x : ℝ) in 0..Real.pi / 2, Real.log (Real.cos x) ^ 2 = ∫ (x : ℝ) in 0..Real.pi / 2, Real.log (Real.sin x) ^ 2

∫₀^{π/2} log² cos x dx = ∫₀^{π/2} log² sin x dx, by x ↦ π/2 - x.

theorem LeanPolyLog.LogSinSq.integral_log_sin_sq_zero_pi : ∫ (x : ℝ) in 0..Real.pi, Real.log (Real.sin x) ^ 2 = 2 * ∫ (x : ℝ) in 0..Real.pi / 2, Real.log (Real.sin x) ^ 2

∫₀^π log² sin x dx = 2 ∫₀^{π/2} log² sin x dx, by x ↦ π - x on [π/2, π].

theorem LeanPolyLog.LogSinSq.integral_log_cos_zero_pi_div_two : ∫ (x : ℝ) in 0..Real.pi / 2, Real.log (Real.cos x) = -(Real.pi / 2 * Real.log 2)

∫₀^{π/2} log sin x dx = ∫₀^{π/2} log cos x dx = -(π/2) log 2.

The substitution x = arctan t

theorem LeanPolyLog.LogSinSq.integral_log_tan_sq : ∫ (x : ℝ) in 0..Real.pi / 4, (Real.log (Real.sin x) - Real.log (Real.cos x)) ^ 2 = Real.pi ^ 3 / 16

∫₀^{π/4} (log sin x - log cos x)² dx = ∫₀¹ log² t/(1+t²) dt = π³/16.

theorem LeanPolyLog.LogSinSq.integral_log_tan_sq_zero_pi_div_two : ∫ (x : ℝ) in 0..Real.pi / 2, (Real.log (Real.sin x) - Real.log (Real.cos x)) ^ 2 = Real.pi ^ 3 / 8

∫₀^{π/2} (log sin x - log cos x)² dx = π³/8: the reflection x ↦ π/2 - x maps [π/4, π/2] onto [0, π/4] and swaps sin and cos.

The value of ∫₀^{π/2} log² sin

theorem LeanPolyLog.LogSinSq.integral_log_sin_sq_and : ∫ (x : ℝ) in 0..Real.pi / 2, Real.log (Real.sin x) ^ 2 = Real.pi ^ 3 / 24 + Real.pi / 2 * Real.log 2 ^ 2 ∧ ∫ (x : ℝ) in 0..Real.pi / 2, Real.log (Real.sin x) * Real.log (Real.cos x) = Real.pi / 2 * Real.log 2 ^ 2 - Real.pi ^ 3 / 48

∫₀^{π/2} log² sin x dx = π³/24 + (π/2) log² 2 and ∫₀^{π/2} log sin x · log cos x dx = (π/2) log² 2 - π³/48.

theorem LeanPolyLog.LogSinSq.integral_log_sin_sq : ∫ (x : ℝ) in 0..Real.pi / 2, Real.log (Real.sin x) ^ 2 = Real.pi ^ 3 / 24 + Real.pi / 2 * Real.log 2 ^ 2

∫₀^{π/2} log² sin x dx = π³/24 + (π/2) log² 2.

theorem LeanPolyLog.LogSinSq.integral_log_sin_mul_log_cos : ∫ (x : ℝ) in 0..Real.pi / 2, Real.log (Real.sin x) * Real.log (Real.cos x) = Real.pi / 2 * Real.log 2 ^ 2 - Real.pi ^ 3 / 48

∫₀^{π/2} log sin x · log cos x dx = (π/2) log² 2 - π³/48.