English
Let s be a finite index set and for each i in s let f_i be an integrable α → G function. Then the integral over α of the sum of the f_i over i ∈ s equals the sum over i ∈ s of the integrals of f_i.
Русский
Пусть s является конечной совокупностью индексов, и для каждого i∈s функция f_i: α → G интегрируема. Тогда интеграл по α от суммы функций f_i по i∈s равен сумме интегралов ∫ f_i.
LaTeX
$$$\int a, \sum_{i \in s} f_i(a) \partial\mu = \sum_{i \in s} \int a, f_i(a) \partial\mu$$$
Lean4
theorem integral_finset_sum {ι} (s : Finset ι) {f : ι → α → G} (hf : ∀ i ∈ s, Integrable (f i) μ) :
∫ a, ∑ i ∈ s, f i a ∂μ = ∑ i ∈ s, ∫ a, f i a ∂μ :=
by
by_cases hG : CompleteSpace G
· simp only [integral, hG, L1.integral]
exact setToFun_finset_sum (dominatedFinMeasAdditive_weightedSMul _) s hf
· simp [integral, hG]
