English
A standard Finset sum version: for integrable f_i indexed by a finite set, setToFun of the sum equals the sum of setToFun of each term.
Русский
Стандартная версия для конечной суммы по индексу: для интегрируемых f_i, сумма внутри setToFun равна сумме отдельных значений.
LaTeX
$$$\forall s: Finset I, \forall (f : I \to α \to E), (\forall i ∈ s, Integrable (f i) μ) \Rightarrow (setToFun μ T hT (\sum i ∈ s, f i) = \sum i ∈ s, setToFun μ T hT (f i))$$$
Lean4
theorem setToFun_finset_sum' (hT : DominatedFinMeasAdditive μ T C) {ι} (s : Finset ι) {f : ι → α → E}
(hf : ∀ i ∈ s, Integrable (f i) μ) : setToFun μ T hT (∑ i ∈ s, f i) = ∑ i ∈ s, setToFun μ T hT (f i) := by
classical
revert hf
refine Finset.induction_on s ?_ ?_
· intro _
simp only [setToFun_zero, Finset.sum_empty]
· intro i s his ih hf
simp only [his, Finset.sum_insert, not_false_iff]
rw [setToFun_add hT (hf i (Finset.mem_insert_self i s)) _]
· rw [ih fun i hi => hf i (Finset.mem_insert_of_mem hi)]
· convert integrable_finset_sum s fun i hi => hf i (Finset.mem_insert_of_mem hi) with x
simp
