Theorems · Definition · measure theory

MeasureTheory.LocallyIntegrableOn

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

A function f : X → E is locally integrable on s, for s ⊆ X, if for every x ∈ s there is a neighbourhood of x within s on which f is integrable. Note that this is, in general, strictly weaker than local integrability with respect to μ.restrict s. For example, fun (x : ℝ) ↦ 1/x is locally integrable on Set.Ioo 0 1 with respect to the Lebesgue measure, but it is not locally integrable with respect to the Lebesgue measure restricted to Set.Ioo 0 1.

Defined in

Mathlib.MeasureTheory.Function.LocallyIntegrable

Cited by

81 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceTopologicalSpaceTopologicalSpaceContinuousENorm