lintegral_finset_sum_measure — Mathlib

English

For a Finset s and a family μ, ∫ f d(sum_{i∈s} μ_i) = ∑_{i∈s} ∫ f dμ_i.

Русский

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

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_finset_sum_measure {ι} (s : Finset ι) (f : α → ℝ≥0∞) (μ : ι → Measure α) :
    ∫⁻ a, f a ∂(∑ i ∈ s, μ i) = ∑ i ∈ s, ∫⁻ a, f a ∂μ i :=
  let F : Measure α →+ ℝ≥0∞ :=
    { toFun := (lintegral · f), map_zero' := lintegral_zero_measure f, map_add' := lintegral_add_measure f }
  map_sum F μ s

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