Theorems · Theorem · measure theory

MeasureTheory.integral_sum_dirac

∀ {ι : 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}
  [FiniteDimensional ℝ E],
  (∀ (i : ι), c i ≠ ⊤) →
    (∫ (x : X), f x ∂MeasureTheory.Measure.sum fun i => c i • MeasureTheory.Measure.dirac (x i)) =
      ∑' (i : ι), (c i).toReal • f (x i)

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

CountableNormedAddCommGroupNormedSpaceMeasurableSingletonClassFiniteDimensional