intervalIntegrable_log — Mathlib

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

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