Theorems · Theorem · measure theory

MeasureTheory.integral_sum_dirac_eq_tsum

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

If the sequence fun i ↦ (c i).toReal * ‖f (x i)‖ is summable, then ∫ x, f x, ∂Measure.sum (fun i ↦ (c i) • .dirac (x i)) = ∑' i, (c i).toReal • f (x i).

Defined in

Mathlib.MeasureTheory.Integral.Bochner.SumMeasure

Cited by

0 results in Mathlib

Foundations

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

Assumes

CountableNormedAddCommGroupNormedSpaceMeasurableSingletonClassCompleteSpace