integral_log_sin_zero_pi — Mathlib

English

Let f(x) = ln(sin x) on [0, π]. Then ∫_0^π f(x) dx = -π ln 2.

Русский

Пусть f(x) = ln(sin x) на [0, π]. Тогда ∫_0^π f(x) dx = -π ln 2.

LaTeX

$$$$\int_{0}^{\pi} \log(\sin x)\,dx = -\pi \log 2.$$$$

Lean4

/-- The integral of `log ∘ sin` on `0 … π` equals `-log 2 * π`.
-/
theorem integral_log_sin_zero_pi : ∫ x in 0..π, log (sin x) = -log 2 * π :=
  by
  rw [integral_log_sin_zero_pi_eq_two_mul_integral_log_sin_zero_pi_div_two, integral_log_sin_zero_pi_div_two]
  ring

Похожие утверждения