sum — Mathlib

English

If each A_i = O_l g for i in a finite set, then the sum over i ∈ s is also O_l g.

Русский

Если для каждого i в конечной совокупности A_i = O_l g, то сумма по i ∈ s тоже равна O_l g.

LaTeX

$$∀ i ∈ s, A_i =O_l g ⇒ (x ↦ ∑_{i∈s} A_i(x)) =O_l g.$$

Lean4

theorem sum (h : ∀ i ∈ s, A i =O[l] g) : (fun x => ∑ i ∈ s, A i x) =O[l] g :=
  by
  simp only [IsBigO_def] at *
  choose! C hC using h
  exact ⟨_, IsBigOWith.sum hC⟩

Похожие утверждения