Theorems · Theorem · measure theory

MeasureTheory.integrable_sum_dirac

∀ {ι : Type u_1} {X : Type u_2} {E : Type u_3} [Countable ι] {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  {f : X → E} [MeasurableSingletonClass X] {x : ι → X} {c : ι → ENNReal},
  (∀ (i : ι), c i ≠ ⊤) →
    (Summable fun i => (c i).toReal * ‖f (x i)‖) →
      MeasureTheory.Integrable f (MeasureTheory.Measure.sum fun i => c i • MeasureTheory.Measure.dirac (x i))

Defined in

Mathlib.MeasureTheory.Integral.Bochner.SumMeasure

Cited by

3 results in Mathlib

Foundations

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

Assumes

CountableNormedAddCommGroupMeasurableSingletonClass