Theorems · Definition · measure theory

MeasureTheory.IntegrableAtFilter

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

We say that a function f is integrable at filter l if it is integrable on some set s ∈ l. Equivalently, it is eventually integrable on s in l.smallSets.

Defined in

Mathlib.MeasureTheory.Integral.IntegrableOn

Cited by

66 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceContinuousENorm