Absolutely summable family
AbsolutelySummabledef
A family is absolutely summable when the sum of the norms converges. This is the hypothesis under which rearrangement is harmless and Fourier series converge uniformly.
def AbsolutelySummable {ι E : Type*} [NormedAddCommGroup E] (f : ι → E) : Prop :=
Summable fun i => ‖f i‖import Conjectura.Defs.Mathematics.Analysis.HarmonicAnalysis.AbsolutelySummable · maintainer — open · raw source
Copyright (c) 2026 The Conjectura Authors. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: The Conjectura Authors