English
If 0 < b, then ∫_0^b log s ds = b log b − b.
Русский
Если 0 < b, то ∫_0^b log s ds = b log b − b.
LaTeX
$$$\forall b>0,\ \displaystyle \int_0^b \log s \, ds = b \log b - b$$$
Lean4
/-- Helper lemma for `integral_log`: case where `a = 0` and `b` is positive. -/
theorem integral_log_from_zero_of_pos (ht : 0 < b) : ∫ s in 0..b, log s = b * log b - b := by
-- Compute the integral by giving a primitive and considering it limit as x approaches 0 from the
-- right. The following lines were suggested by Gareth Ma on Zulip.
rw [integral_eq_sub_of_hasDerivAt_of_tendsto (f := fun x ↦ x * log x - x) (fa := 0) (fb := b * log b - b) (hint :=
intervalIntegrable_log')]
· abel
· exact ht
· intro s ⟨hs, _⟩
simpa using (hasDerivAt_mul_log hs.ne.symm).sub (hasDerivAt_id s)
·
simpa [mul_comm] using
((tendsto_log_mul_rpow_nhdsGT_zero zero_lt_one).sub (tendsto_nhdsWithin_of_tendsto_nhds Filter.tendsto_id))
· exact tendsto_nhdsWithin_of_tendsto_nhds (ContinuousAt.tendsto (by fun_prop))
