Partial sums of a family with at most one nonzero term

If a family u in a seminormed group has at most one nonzero term, then every finite partial sum is either the whole sum or zero, so it differs from ∑' i, u i by at most ‖∑' i, u i‖ₑ (Set.Subsingleton.enorm_sum_sub_tsum_le). Such a uniform bound on the partial sums is what dominated convergence needs to pass from pointwise to Lᵖ convergence of a sum of functions with pairwise disjoint supports.

For families f and y in seminormed groups with ∑ i, ‖f i‖ * ‖y i‖ summable, the extended sum ∑' i, ‖f i‖ₑ * ‖y i‖ₑ is the extended real ENNReal.ofReal (∑' i, ‖f i‖ * ‖y i‖) (TauCeti.tsum_enorm_mul_enorm_eq_ofReal).

theorem Set.Subsingleton.enorm_sum_sub_tsum_le {κ : Type u_1} {E : Type u_2} [SeminormedAddCommGroup E] {u : κ → E} (hu : (Function.support u).Subsingleton) (s : Finset κ) : ‖∑ i ∈ s, u i - ∑' (i : κ), u i‖ₑ ≤ ‖∑' (i : κ), u i‖ₑ

If a family has at most one nonzero term, each finite partial sum differs from the sum by at most the extended norm of the sum.

theorem TauCeti.tsum_enorm_mul_enorm_eq_ofReal {ι : Type u_1} {G : Type u_2} {H : Type u_3} [SeminormedAddGroup G] [SeminormedAddGroup H] {f : ι → G} {y : ι → H} (hfy : Summable fun (i : ι) => ‖f i‖ * ‖y i‖) : ∑' (i : ι), ‖f i‖ₑ * ‖y i‖ₑ = ENNReal.ofReal (∑' (i : ι), ‖f i‖ * ‖y i‖)

If ∑ i, ‖f i‖ * ‖y i‖ is summable, the extended sum ∑' i, ‖f i‖ₑ * ‖y i‖ₑ is its real sum viewed as an extended real.