Theorems · Theorem · measure theory

MeasureTheory.hasSum_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} [CompleteSpace E],
  (∀ (i : ι), c i ≠ ⊤) →
    (Summable fun i => (c i).toReal * ‖f (x i)‖) →
      HasSum (fun i => (c i).toReal • f (x i))
        (∫ (x : X), f x ∂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 259 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CountableNormedAddCommGroupNormedSpaceMeasurableSingletonClassCompleteSpace