Theorems · Definition · measure theory

MeasureTheory.Integrable

{ε : Type u_5} →
  [inst : TopologicalSpace ε] →
    [ContinuousENorm ε] →
      {α : Type u_8} →
        {x : MeasurableSpace α} → (α → ε) → autoParam (MeasureTheory.Measure α) MeasureTheory.Integrable._auto_1 → Prop

Integrable f μ means that f is measurable and that the integral ∫⁻ a, ‖f a‖ ∂μ is finite. Integrable f means Integrable f volume.

Defined in

Mathlib.MeasureTheory.Function.L1Space.Integrable

Cited by

1,367 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceContinuousENorm