Theorems · Definition · measure theory

IntervalIntegrable

{ε : Type u_3} → [inst : TopologicalSpace ε] → [ENormedAddMonoid ε] → (ℝ → ε) → MeasureTheory.Measure ℝ → ℝ → ℝ → Prop

A function f is called interval integrable with respect to a measure μ on an unordered interval a..b if it is integrable on both intervals (a, b] and (b, a]. One of these intervals is always empty, so this property is equivalent to f being integrable on (min a b, max a b].

Defined in

Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic

Cited by

316 results in Mathlib

Foundations

Depth 194 from the axioms, rests on 4,795 definitions · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceENormedAddMonoid