integral_finset_sum — Mathlib

English

For a finite index set Finset s and functions f_i, the integral of the finite sum equals the finite sum of integrals, provided each f_i is interval-integrable on [a,b].

Русский

Для конечного множества индексов и функций f_i интеграл суммы равен сумме интегралов при условии интегрируемости каждого f_i на [a,b].

LaTeX

$$$\int_{a}^{b} \sum_{i\in s} f_i(x) \, dμ = \sum_{i\in s} \int_{a}^{b} f_i(x) \, dμ$$$

Lean4

nonrec theorem integral_finset_sum {ι} {s : Finset ι} {f : ι → ℝ → E} (h : ∀ i ∈ s, IntervalIntegrable (f i) μ a b) :
    ∫ x in a..b, ∑ i ∈ s, f i x ∂μ = ∑ i ∈ s, ∫ x in a..b, f i x ∂μ := by
  simp only [intervalIntegral_eq_integral_uIoc, integral_finset_sum s fun i hi => (h i hi).def', Finset.smul_sum]

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