Theorems · Theorem · approximation theory

Asymptotics.IsBigOWith.sum_congr

∀ {α : Type u_1} {E' : Type u_6} [inst : SeminormedAddCommGroup E'] {l : Filter α} {ι : Type u_18} {A : ι → α → E'}
  {C : ι → ℝ} {s : Finset ι} {B : ι → α → ℝ},
  (∀ i ∈ s, Asymptotics.IsBigOWith (C i) l (A i) (B i)) →
    Asymptotics.IsBigOWith (sSup (C '' ↑s)) l (fun H => ∑ i ∈ s, A i H) fun H => ∑ i ∈ s, ‖B i H‖

If each term A i of a sum IsBigO of B i, then the sum of the A i IsBigO of the sum of the norms of the B i.

Defined in

Mathlib.Analysis.Asymptotics.Defs

Cited by

1 results in Mathlib

Foundations

Depth 157 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SeminormedAddCommGroup