Integrals of Functions Prominently Involving the Logarithm

Integral of log ∘ sin

This file computes special values of the integral of log ∘ sin. Given that the indefinite integral involves the dilogarithm, this can be seen as computing special values of Li₂.

theorem integral_log_sin_zero_pi_div_two : ∫ (x : ℝ) in 0..Real.pi / 2, Real.log (Real.sin x) = -Real.log 2 * Real.pi / 2

The integral of log ∘ sin on 0 … π/2 equals -log 2 * π / 2.

theorem integral_log_sin_zero_pi : ∫ (x : ℝ) in 0..Real.pi, Real.log (Real.sin x) = -Real.log 2 * Real.pi

The integral of log ∘ sin on 0 … π equals -log 2 * π.