integral_finset_sum_measure — Mathlib

English

For a finite index set s, integrating against the sum of measures equals the finite sum of integrals: ∫ f d(∑ i∈s μ_i) = ∑ i∈s ∫ f dμ_i.

Русский

Для конечного множества индексов s интеграл по сумме мер равен сумме интегралов: ∫ f d(∑_{i∈s} μ_i) = ∑_{i∈s} ∫ f dμ_i.

LaTeX

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

Lean4

theorem integral_finset_sum_measure {ι} {m : MeasurableSpace α} {f : α → G} {μ : ι → Measure α} {s : Finset ι}
    (hf : ∀ i ∈ s, Integrable f (μ i)) : ∫ a, f a ∂(∑ i ∈ s, μ i) = ∑ i ∈ s, ∫ a, f a ∂μ i := by
  induction s using Finset.cons_induction_on with
  | empty => simp
  | cons _ _ h ih =>
    rw [Finset.forall_mem_cons] at hf
    rw [Finset.sum_cons, Finset.sum_cons, ← ih hf.2]
    exact integral_add_measure hf.1 (integrable_finset_sum_measure.2 hf.2)

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