English
For real a ≤ b with appropriate domain, ∫_a^b log s ds equals b log b − a log a − b + a.
Русский
Пусть a ≤ b и все сомножители определены; тогда ∫_a^b log s ds = b log b − a log a − b + a.
LaTeX
$$$\forall a,b \in \mathbb{R},\ \displaystyle \int_a^b \log s \, ds = b \log b - a \log a - b + a$$$
Lean4
@[simp]
theorem integral_log : ∫ s in a..b, log s = b * log b - a * log a - b + a :=
by
rw [← intervalIntegral.integral_add_adjacent_intervals (b := 0)]
· rw [intervalIntegral.integral_symm, integral_log_from_zero, integral_log_from_zero]
ring
all_goals exact intervalIntegrable_log'