Theorems · Theorem · measure theory

MeasureTheory.integrable_of_summable_norm_restrict

∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} {ι : Type u_5} [Countable ι] {μ : MeasureTheory.Measure X}
  [inst : NormedAddCommGroup E] [inst_1 : TopologicalSpace X] [BorelSpace X] [T2Space X]
  [MeasureTheory.IsLocallyFiniteMeasure μ] {f : C(X, E)} {s : ι → TopologicalSpace.Compacts X},
  (Summable fun i => ‖ContinuousMap.restrict (↑(s i)) f‖ * μ.real ↑(s i)) →
    ⋃ i, ↑(s i) = Set.univ → MeasureTheory.Integrable (⇑f) μ

If s is a countable family of compact sets covering X, f is a continuous function, and the sequence ‖f.restrict (s i)‖ * μ (s i) is summable, then f is integrable.

Defined in

Mathlib.MeasureTheory.Integral.Bochner.Set

Cited by

1 results in Mathlib

Foundations

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

Assumes

CountableNormedAddCommGroupTopologicalSpaceBorelSpaceT2SpaceMeasureTheory.IsLocallyFiniteMeasure