English
If (f_i) is a countable family of nonnegative functions and each f_i is a.e. measurable, then the lintegral commutes with the tsum: ∫⁻ ∑' i f_i = ∑' i ∫⁻ f_i.
Русский
Пусть имеется счетная последовательность функций неотрицательных; если каждая функция измерима почти всюду, то линеграл обращается со суммой по i: ∫⁻ ∑ f_i = ∑ ∫⁻ f_i.
LaTeX
$$$[Countable \beta] \; \forall f : \beta \to (\alpha \to \mathbb{R}_{\ge 0}^{\infty}),\; (\forall i, AEMeasurable (f i) \mu) \Rightarrow ∫^- a, \sum_i f i a \partial\mu = \sum_i ∫^- a, f i a \partial\mu$$$
Lean4
theorem lintegral_tsum [Countable β] {f : β → α → ℝ≥0∞} (hf : ∀ i, AEMeasurable (f i) μ) :
∫⁻ a, ∑' i, f i a ∂μ = ∑' i, ∫⁻ a, f i a ∂μ := by
classical
simp only [ENNReal.tsum_eq_iSup_sum]
rw [lintegral_iSup_directed]
· simp [lintegral_finset_sum' _ fun i _ => hf i]
· intro b
exact Finset.aemeasurable_fun_sum _ fun i _ => hf i
· intro s t
use s ∪ t
constructor
· exact fun a => Finset.sum_le_sum_of_subset Finset.subset_union_left
· exact fun a => Finset.sum_le_sum_of_subset Finset.subset_union_right
