Absolutely summable family

Conjectura.Defs.Mathematics.Analysis.HarmonicAnalysis.AbsolutelySummable

/-
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
-/
import Mathlib.Topology.Algebra.InfiniteSum.Defs
import Mathlib.Analysis.Normed.Group.Basic

/-! # Absolutely summable family -/

namespace Conjectura.HarmonicAnalysis

/-- 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‖

end Conjectura.HarmonicAnalysis