English
If for every i in a Finset α we have HasIntegral I l (f i) vol (g i), then HasIntegral I l (sum over i of f i) vol (sum over i of g i).
Русский
Если для каждого i из конечного множества α верно HasIntegral I l (f i) vol (g i), то HasIntegral I l (∑ i∈α f i) vol (∑ i∈α g i).
LaTeX
$$$\big(\forall i, i\in s \Rightarrow HasIntegral I l (f i) vol (g i)\big) \Rightarrow HasIntegral I l (\sum i\in s, f i) vol (\sum i\in s, g i)$$$
Lean4
theorem sum {α : Type*} {s : Finset α} {f : α → ℝⁿ → E} {g : α → F} (h : ∀ i ∈ s, HasIntegral I l (f i) vol (g i)) :
HasIntegral I l (fun x => ∑ i ∈ s, f i x) vol (∑ i ∈ s, g i) := by
classical
induction s using Finset.induction_on with
| empty => simp [hasIntegral_zero]
| insert a s ha ihs =>
simp only [Finset.sum_insert ha]; rw [Finset.forall_mem_insert] at h
exact h.1.add (ihs h.2)
