integral_sum_measure — Mathlib

English

The integral over the sum of measures equals the sum of integrals: ∫ f d(∑ μ_i) = ∑' i, ∫ f dμ_i.

Русский

Интеграл по сумме мер равен сумме интегралов: ∫ f d(∑ μ_i) = ∑' i, ∫ f dμ_i.

LaTeX

$$$$\int a, f(a) \partial(\sum_i μ_i) = \sum' i, \int a, f(a) \partial μ_i.$$$$

Lean4

theorem integral_sum_measure {ι} {_ : MeasurableSpace α} {f : α → G} {μ : ι → Measure α}
    (hf : Integrable f (Measure.sum μ)) : ∫ a, f a ∂Measure.sum μ = ∑' i, ∫ a, f a ∂μ i :=
  (hasSum_integral_measure hf).tsum_eq.symm

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