English
If each A_i = O_l g with corresponding constants C_i, then the finite sum over i ∈ s satisfies the same Big-O relation with total bound ∑ C_i.
Русский
Если каждое A_i = O_l g с константой C_i, то сумма по i ∈ s также удовлетворяет той же связи Big-O с суммой констант ∑ C_i.
LaTeX
$$$\\forall i ∈ s,\ A_i =O_l g \\Rightarrow (x \\mapsto \\sum_{i∈s} A_i(x)) =O_l g.$$$
Lean4
theorem sum (h : ∀ i ∈ s, IsBigOWith (C i) l (A i) g) : IsBigOWith (∑ i ∈ s, C i) l (fun x => ∑ i ∈ s, A i x) g := by
induction s using Finset.cons_induction with
| empty => simp only [isBigOWith_zero', Finset.sum_empty]
| cons i s is IH =>
simp only [Finset.sum_cons, Finset.forall_mem_cons] at h ⊢
exact h.1.add (IH h.2)
