English
For a Finset s and a family of functions f b, the lintegral of the pointwise finite sum equals the finite sum of lintegrals, provided each f b is a.e. measurable.
Русский
Для конечного множества s и семейства функций f_b верно, что линеграл суммы по точкам равен сумме линегралов, при условии, что каждый f_b измерим почти всюду.
LaTeX
$$$\forall s : Finset \beta, \forall f : \beta \to (\alpha \to \mathbb{R}_{\ge 0}^{\infty}),\; (\forall b \in s, AEMeasurable (f b) \mu) \Rightarrow ∫^- a, \sum_{b \in s} f b a \partial\mu = \sum_{b \in s} ∫^- a, f b a \partial\mu$$$
Lean4
theorem lintegral_finset_sum' (s : Finset β) {f : β → α → ℝ≥0∞} (hf : ∀ b ∈ s, AEMeasurable (f b) μ) :
∫⁻ a, ∑ b ∈ s, f b a ∂μ = ∑ b ∈ s, ∫⁻ a, f b a ∂μ := by
classical
induction s using Finset.induction_on with
| empty => simp
| insert a s has ih =>
simp only [Finset.sum_insert has]
rw [Finset.forall_mem_insert] at hf
rw [lintegral_add_left' hf.1, ih hf.2]
