Theorems · Definition · measure theory

MeasureTheory.IntegrableOn

{α : Type u_1} →
  {ε : Type u_3} →
    {mα : MeasurableSpace α} →
      [inst : TopologicalSpace ε] →
        [ContinuousENorm ε] →
          (α → ε) → Set α → autoParam (MeasureTheory.Measure α) MeasureTheory.IntegrableOn._auto_1 → Prop

A function is IntegrableOn a set s if it is almost everywhere strongly measurable on s and if the integral of its pointwise norm over s is less than infinity.

Defined in

Mathlib.MeasureTheory.Integral.IntegrableOn

Cited by

548 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceContinuousENorm