Infinite sum over a topological monoid

This sum is known as unconditionally convergent, as it sums to the same value under all possible permutations. For Euclidean spaces (finite dimensional Banach spaces) this is equivalent to absolute convergence.

Note: There are summable sequences which are not unconditionally convergent! The other way holds generally, see HasSum.tendsto_sum_nat.

References

• Bourbaki: General Topology (1995), Chapter 3 §5 (Infinite sums in commutative groups)

def HasSum {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (f : β → α) (a : α) : Prop

Infinite sum on a topological monoid

The atTop filter on Finset β is the limit of all finite sets towards the entire type. So we sum up bigger and bigger sets. This sum operation is invariant under reordering. In particular, the function ℕ → ℝ sending n to (-1)^n / (n+1) does not have a sum for this definition, but a series which is absolutely convergent will have the correct sum.

This is based on Mario Carneiro's infinite sum df-tsms in Metamath.

For the definition or many statements, α does not need to be a topological monoid. We only add this assumption later, for the lemmas where it is relevant.

Equations

• HasSum f a = Filter.Tendsto (fun (s : Finset β) => Finset.sum s fun (b : β) => f b) Filter.atTop (nhds a)

def Summable {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (f : β → α) : Prop

Summable f means that f has some (infinite) sum. Use tsum to get the value.

Equations

• Summable f = ∃ (a : α), HasSum f a

@[irreducible]

def tsum {α : Type u_4} [AddCommMonoid α] [TopologicalSpace α] {β : Type u_5} (f : β → α) : α

∑' i, f i is the sum of f it exists, or 0 otherwise.

Equations

• @tsum = wrapped✝.1

theorem tsum_def {α : Type u_4} [AddCommMonoid α] [TopologicalSpace α] {β : Type u_5} (f : β → α) : tsum f = if h : Summable f then if Set.Finite (Function.support f) then finsum f else Exists.choose h else 0

def «term∑'_,_».delab : Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

Equations

• One or more equations did not get rendered due to their size.

def «term∑'_,_» : Lean.ParserDescr

∑' i, f i is the sum of f it exists, or 0 otherwise.

Equations

• One or more equations did not get rendered due to their size.

theorem HasSum.summable {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} (h : HasSum f a) : Summable f

theorem tsum_eq_zero_of_not_summable {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} (h : ¬Summable f) : ∑' (b : β), f b = 0

theorem Function.Injective.hasSum_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} {g : γ → β} (hg : Function.Injective g) (hf : ∀ x ∉ Set.range g, f x = 0) : HasSum (f ∘ g) a ↔ HasSum f a

theorem hasSum_subtype_iff_of_support_subset {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} {s : Set β} (hf : Function.support f ⊆ s) : HasSum (f ∘ Subtype.val) a ↔ HasSum f a

theorem hasSum_fintype {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] [Fintype β] (f : β → α) : HasSum f (Finset.sum Finset.univ fun (b : β) => f b)

theorem Finset.hasSum {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (s : Finset β) (f : β → α) : HasSum (f ∘ Subtype.val) (Finset.sum s fun (b : β) => f b)

theorem hasSum_sum_of_ne_finset_zero {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {s : Finset β} (hf : ∀ b ∉ s, f b = 0) : HasSum f (Finset.sum s fun (b : β) => f b)

If a function f vanishes outside of a finite set s, then it HasSum ∑ b in s, f b.

theorem summable_of_ne_finset_zero {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {s : Finset β} (hf : ∀ b ∉ s, f b = 0) : Summable f

theorem Summable.hasSum {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} (ha : Summable f) : HasSum f (∑' (b : β), f b)

theorem HasSum.unique {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {a₁ : α} {a₂ : α} [T2Space α] : HasSum f a₁ → HasSum f a₂ → a₁ = a₂

theorem HasSum.tsum_eq {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} [T2Space α] (ha : HasSum f a) : ∑' (b : β), f b = a

theorem Summable.hasSum_iff {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] {f : β → α} {a : α} [T2Space α] (h : Summable f) : HasSum f a ↔ ∑' (b : β), f b = a