Theorems · Theorem · functional analysis

tsum_of_norm_bounded

∀ {ι : Type u_1} {E : Type u_3} [inst : SeminormedAddCommGroup E] {f : ι → E} {g : ι → ℝ} {a : ℝ},
  HasSum g a → (∀ (i : ι), ‖f i‖ ≤ g i) → ‖∑' (i : ι), f i‖ ≤ a

Quantitative result associated to the direct comparison test for series: If ∑' i, g i is summable, and for all i, ‖f i‖ ≤ g i, then ‖∑' i, f i‖ ≤ ∑' i, g i. Note that we do not assume that ∑' i, f i is summable, and it might not be the case if α is not a complete space.

Defined in

Mathlib.Analysis.Normed.Group.InfiniteSum

Cited by

7 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroup