Theorems · Definition · measure theory

MeasureTheory.LocallyIntegrable

{X : Type u_1} →
  {ε : Type u_3} →
    [inst : MeasurableSpace X] →
      [TopologicalSpace X] →
        [inst_2 : TopologicalSpace ε] →
          [ContinuousENorm ε] →
            (X → ε) → autoParam (MeasureTheory.Measure X) MeasureTheory.LocallyIntegrable._auto_1 → Prop

A function f : X → ε is locally integrable if it is integrable on a neighborhood of every point. In particular, it is integrable on all compact sets, see LocallyIntegrable.integrableOn_isCompact.

Defined in

Mathlib.MeasureTheory.Function.LocallyIntegrable

Cited by

90 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceTopologicalSpaceTopologicalSpaceContinuousENorm