Theorems · Theorem · measure theory

MeasureTheory.integrable_sum_dirac_iff

∀ {ι : 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 ≠ ⊤) →
    (MeasureTheory.Integrable f (MeasureTheory.Measure.sum fun i => c i • MeasureTheory.Measure.dirac (x i)) ↔
      Summable fun i => (c i).toReal * ‖f (x i)‖)

A function f is integrable with respect to a countable sum of Dirac masses Measure.sum (fun i ↦ (c i) • Measure.dirac (x i)) if and only if the sequence fun i ↦ (c i).toReal * ‖f (x i)‖ is summable.

Defined in

Mathlib.MeasureTheory.Integral.Bochner.SumMeasure

Cited by

2 results in Mathlib

Foundations

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

Assumes

CountableNormedAddCommGroupMeasurableSingletonClass