Theorems · Theorem · real analysis

intervalIntegral.intervalIntegrable_log

∀ {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ],
  0 ∉ Set.uIcc a b → IntervalIntegrable Real.log μ a b

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.

Defined in

Mathlib.Analysis.SpecialFunctions.Integrability.Basic

Cited by

0 results in Mathlib

Foundations

Depth 210 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasureTheory.IsLocallyFiniteMeasure