Theorems · Theorem · measure theory

MeasureTheory.hasSum_integral_measure

∀ {ι : Type u_1} {X : Type u_2} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  {μ : ι → MeasureTheory.Measure X} {f : X → E} [inst_1 : NormedSpace ℝ E],
  MeasureTheory.Integrable f (MeasureTheory.Measure.sum μ) →
    HasSum (fun i => ∫ (x : X), f x ∂μ i) (∫ (x : X), f x ∂MeasureTheory.Measure.sum μ)

If f is integrable with respect to Measure.sum μ, then the sequence fun i ↦ ∫ x, f x ∂μ i is summable and its sum is ∫ x, f x ∂Measure.sum μ.

Defined in

Mathlib.MeasureTheory.Integral.Bochner.SumMeasure

Cited by

4 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace