Theorems · Theorem · approximation theory

Asymptotics.IsLittleO.sum_range

∀ {α : Type u_1} [inst : NormedAddCommGroup α] {f : ℕ → α} {g : ℕ → ℝ},
  f =o[Filter.atTop] g →
    0 ≤ g →
      Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, g i) Filter.atTop Filter.atTop →
        (fun n => ∑ i ∈ Finset.range n, f i) =o[Filter.atTop] fun n => ∑ i ∈ Finset.range n, g i

Defined in

Mathlib.Analysis.Asymptotics.SpecificAsymptotics

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroup