lintegral_sum_measure — Mathlib

English

If s is a finite set, then the lintegral over the sum of measures equals the sum of the individual lintegrals.

Русский

Для конечного множества верно: линегерал по сумме мер равен сумме соответствующих линегралов.

LaTeX

$$$\\int f \\, d\\left(\\sum_{i\\in s} \\mu_i\\right) = \\sum_{i\\in s} \\int f \\, d\\mu_i$$$

Lean4

@[simp]
theorem lintegral_sum_measure {m : MeasurableSpace α} {ι} (f : α → ℝ≥0∞) (μ : ι → Measure α) :
    ∫⁻ a, f a ∂Measure.sum μ = ∑' i, ∫⁻ a, f a ∂μ i := by
  simp_rw [ENNReal.tsum_eq_iSup_sum, ← lintegral_finset_sum_measure, lintegral, SimpleFunc.lintegral_sum,
    ENNReal.tsum_eq_iSup_sum, SimpleFunc.lintegral_finset_sum, iSup_comm (ι := Finset ι)]

Похожие утверждения