integral_log — Mathlib

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'

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