Theorems · Theorem · functional analysis

tsum_of_enorm_bounded

∀ {ι : Type u_1} {ε : Type u_5} [inst : TopologicalSpace ε] [inst_1 : ESeminormedAddCommMonoid ε] {f : ι → ε}
  {g : ι → ENNReal} {a : ENNReal}, HasSum g a → (∀ (i : ι), ‖f i‖ₑ ≤ g i) → ‖∑' (i : ι), f i‖ₑ ≤ a

Quantitative result associated to the direct comparison test for series: If, 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

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceESeminormedAddCommMonoid