Theorems · Definition · sequences and series

HasSum

{α : Type u_1} →
  {β : Type u_2} →
    [AddCommMonoid α] →
      [TopologicalSpace α] → (β → α) → α → optParam (SummationFilter β) (SummationFilter.unconditional β) → Prop

HasSum f a L means that the (potentially infinite) sum of the f b for b : β converges to a along the SummationFilter L. By default L is the unconditional one, corresponding to the limit of all finite sets towards the entire type. So we take the sum over bigger and bigger finite sets. This sum operation is invariant under permuting the terms (while sums for more general summation filters usually are not). This is based on Mario Carneiro's [infinite sum df-tsms in Metamath](http://us.metamath.org/mpeuni/df-tsms.html). In particular, the function ℕ → ℝ sending n to (-1) ^ n / (n + 1) does not have a sum for this definition, although it is summable for the conditional summation filter that takes limits of sums over n ∈ {0, ..., X} as X → ∞. However, a series which is absolutely convergent with respect to the conditional summation filter is in fact unconditionally summable. For the definition and many statements, α does not need to be a topological additive monoid, only an additive monoid with a topology (i.e. the addition is not assumed to be continuous). We only add this assumption later, for the lemmas where it is relevant.

Defined in

Mathlib.Topology.Algebra.InfiniteSum.Defs

Cited by

518 results in Mathlib

Foundations

Depth 56 from the axioms, rests on 923 definitions · uses propext, Classical.choice, Quot.sound

Assumes

AddCommMonoidTopologicalSpace