English
The real logarithm is interval-integrable on the entire interval [a,b] in volume measure.
Русский
Логарифм по Лебегу интегрируем на любом интервале [a,b] по объему.
LaTeX
$$$\text{IntervalIntegrable } \log \text{ на } [a,b]$$$
Lean4
/-- The real logarithm is interval integrable (with respect to every locally finite measure) over every
interval that does not contain zero. See `intervalIntegrable_log'` for a version without any
hypothesis on the interval, but assuming the measure is the volume.
-/
@[simp]
theorem intervalIntegrable_log (h : (0 : ℝ) ∉ [[a, b]]) : IntervalIntegrable log μ a b :=
IntervalIntegrable.log continuousOn_id fun _ hx => ne_of_mem_of_not_mem hx h