Theorems · Theorem · functional analysis

summable_norm_iff

∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E]
  {f : α → E}, (Summable fun x => ‖f x‖) ↔ Summable f

In a finite-dimensional vector space over ℝ, the series ∑ x, ‖f x‖ is unconditionally summable if and only if the series ∑ x, f x is unconditionally summable. One implication holds in any complete normed space, while the other holds only in finite-dimensional spaces.

Defined in

Mathlib.Analysis.Normed.Module.FiniteDimension

Cited by

8 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceFiniteDimensional