Theorems · Theorem · sequences and series

tsum_def

∀ {α : Type u_4} {β : Type u_5} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] (f : β → α)
  (L : SummationFilter β),
  tsum f L =
    if h : Summable f L then
      if L.HasSupport ∧ (Function.support f ∩ L.support).Finite then finsum (L.support.indicator f)
      else if HasSum f 0 L then 0 else Exists.choose h
    else 0

∑' i, f i is the unconditional sum of f if it exists, or 0 otherwise. More generally, if L is a SummationFilter, ∑'[L] i, f i is the sum of f with respect to L if it exists, and 0 otherwise. (Note that even if the unconditional sum exists, it might not be unique if the topology is not separated. When the support of f is finite, we make the most reasonable choice, to use the sum over the support. Otherwise, we choose arbitrarily an a satisfying HasSum f a. Similar remarks apply to more general summation filters.)

Defined in

Mathlib.Topology.Algebra.InfiniteSum.Defs

Cited by

11 results in Mathlib

Foundations

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

Assumes

AddCommMonoidTopologicalSpace