A009: ∫₀^{π/2} x² cot x dx = (π²/4) log 2 - (7/8) ζ(3)

Let J = ∫₀^{π/2} x log sin x dx.

• Split [0, π/2] at π/4. With x ↦ π/2 - x the upper half is ∫₀^{π/4} (π/2 - u) log cos u du.
• On the lower half, sin x = sin 2x / (2 cos x), and u = 2x gives ∫₀^{π/4} x log sin 2x dx = J/4.
• Together: (3/4) J = -(π²/32) log 2 - 2 ∫₀^{π/4} x log cos x + (π/2) ∫₀^{π/4} log cos x, so A006 and A007 give J = -(π²/8) log 2 + (7/16) ζ(3).

Finally F x = x² log sin x is continuous on [0, π/2] (it tends to 0 at 0), vanishes at both ends, and has derivative 2x log sin x + x² cot x on (0, π/2). Hence A009 = -2J.

In Lean cot 0 = 0 and log 0 = 0; single points do not affect the integrals. The helper lemmas and integral_mul_log_sin (the value of J) are public, and A011 reuses them.

theorem LeanPolyLog.Proofs.sq_le_mul_sin {x : ℝ} (hx : x ∈ Set.Icc 0 (Real.pi / 2)) : x ^ 2 ≤ Real.pi ^ 2 / 4 * Real.sin x

x² ≤ (π²/4) sin x on [0, π/2], from Jordan's inequality (2/π) x ≤ sin x.

theorem LeanPolyLog.Proofs.continuousOn_sq_mul_log_sin : ContinuousOn (fun (x : ℝ) => x ^ 2 * Real.log (Real.sin x)) (Set.Icc 0 (Real.pi / 2))

x ↦ x² log sin x is continuous on [0, π/2]. At 0 it tends to 0, because |x² log sin x| ≤ (π²/4) |sin x log sin x| there.

theorem LeanPolyLog.Proofs.intervalIntegrable_sq_mul_cot : IntervalIntegrable (fun (x : ℝ) => x ^ 2 * Real.cot x) MeasureTheory.volume 0 (Real.pi / 2)

x² cot x is integrable on [0, π/2], since it is bounded by π²/4 there.

theorem LeanPolyLog.Proofs.integral_mul_log_sin : ∫ (x : ℝ) in 0..Real.pi / 2, x * Real.log (Real.sin x) = -(Real.pi ^ 2 / 8 * Real.log 2) + 7 / 16 * zeta3

∫₀^{π/2} x log sin x dx = -(π²/8) log 2 + (7/16) ζ(3).

theorem LeanPolyLog.Proofs.A009 : ∫ (x : ℝ) in 0..Real.pi / 2, x ^ 2 * Real.cot x = Real.pi ^ 2 / 4 * Real.log 2 - 7 / 8 * zeta3

A009: ∫₀^{π/2} x² cot x dx = (π²/4) log 2 - (7/8) ζ(3).