lintegral_finset_sum — Mathlib

English

For a simple f, a family of measures μ_i, and a finite set s, the lintegral over the sum equals the finite sum of lintegrals: f.lintegral(∑_{i∈s} μ_i) = ∑_{i∈s} f.lintegral(μ_i).

Русский

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

LaTeX

$$$f.lintegral\\left(\\sum_{i\\in s} \\mu_i\\right) = \\sum_{i\\in s} f.lintegral(\\mu_i)$$$

Lean4

theorem lintegral_finset_sum {ι} (f : α →ₛ ℝ≥0∞) (μ : ι → Measure α) (s : Finset ι) :
    f.lintegral (∑ i ∈ s, μ i) = ∑ i ∈ s, f.lintegral (μ i) :=
  map_sum (lintegralₗ f) ..

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