English
For any b ∈ ℝ, the integral ∫_0^b log s ds equals b log b − b (with the appropriate interpretation across signs).
Русский
Для любого b ∈ ℝ интеграл ∫_0^b log s ds равен b log b − b (с корректной трактовкой по знаку).
LaTeX
$$$\forall b \in \mathbb{R},\ \displaystyle \int_0^b \log s \, ds = b \log b - b$$$
Lean4
/-- Helper lemma for `integral_log`: case where `a = 0`. -/
theorem integral_log_from_zero {b : ℝ} : ∫ s in 0..b, log s = b * log b - b :=
by
rcases lt_trichotomy b 0 with h | h | h
· -- If t is negative, use that log is an even function to reduce to the positive case.
conv => arg 1; arg 1; intro t; rw [← log_neg_eq_log]
rw [intervalIntegral.integral_comp_neg, intervalIntegral.integral_symm, neg_zero,
integral_log_from_zero_of_pos (Left.neg_pos_iff.mpr h), log_neg_eq_log]
ring
· simp [h]
· exact integral_log_from_zero_of_pos h
